Theorem aceq5 3563

Description: Equivalence of two versions of the Axiom of Choice. The left-hand side is similar to the Axiom of Choice (first form) of [Enderton] p. 49. The right-hand side is Theorem 6M(4) of [Enderton] p. 151 and asserts that given a family of mutually disjoint nonempty sets, a set exists containing exactly one member from each set in the family. The proof does not depend on AC.

Assertion

Ref	Expression
aceq5	⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) ↔ ∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))

Distinct variable group(s):   x,f,z,y,w,v

Proof of Theorem aceq5

Step	Hyp	Ref	Expression
1		aceq4 3557	. . 3 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) ↔ ∀x∃f(f Fn x ∧ ∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w)))
2		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = t → (f ‘w) = (f ‘t))
3		id 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = t → w = t)
4	2, 3	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (w = t → ((f ‘w) ∈ w ↔ (f ‘t) ∈ t))
5		cleq2 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = t → (z = w ↔ z = t))
6	5	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = t → (¬ z = w ↔ ¬ z = t))
7		ineq2 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = t → (z ∩ w) = (z ∩ t))
8	7	cleq1d 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = t → ((z ∩ w) = ∅ ↔ (z ∩ t) = ∅))
9	6, 8	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (w = t → ((¬ z = w → (z ∩ w) = ∅) ↔ (¬ z = t → (z ∩ t) = ∅)))
10	4, 9	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (w = t → (((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) ↔ ((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅))))
11	10	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → (t ∈ x → ((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅))))
12		disj 1733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((z ∩ t) = ∅ ↔ ∀v ∈ z ¬ v ∈ t)
13		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (v = (f ‘t) → (v ∈ t ↔ (f ‘t) ∈ t))
14	13	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (v = (f ‘t) → (¬ v ∈ t ↔ ¬ (f ‘t) ∈ t))
15	14	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∀v ∈ z ¬ v ∈ t → ((f ‘t) ∈ z → ¬ (f ‘t) ∈ t))
16	12, 15	sylbi 174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((z ∩ t) = ∅ → ((f ‘t) ∈ z → ¬ (f ‘t) ∈ t))
17	16	con2d 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((z ∩ t) = ∅ → ((f ‘t) ∈ t → ¬ (f ‘t) ∈ z))
18	17	com12 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((f ‘t) ∈ t → ((z ∩ t) = ∅ → ¬ (f ‘t) ∈ z))
19	18	syl3d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((f ‘t) ∈ t → ((¬ z = t → (z ∩ t) = ∅) → (¬ z = t → ¬ (f ‘t) ∈ z)))
20	19	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) → (¬ z = t → ¬ (f ‘t) ∈ z))
21	20	a3d 70	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) → ((f ‘t) ∈ z → z = t))
22	21	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) ∧ (f ‘t) ∈ z) → z = t)
23		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f ‘t) = v → ((f ‘t) ∈ z ↔ v ∈ z))
24	23	biimpar 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((f ‘t) = v ∧ v ∈ z) → (f ‘t) ∈ z)
25	22, 24	sylan2 346	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) ∧ ((f ‘t) = v ∧ v ∈ z)) → z = t)
26		cleq2 1110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((f ‘t) = v → ((f ‘z) = (f ‘t) ↔ (f ‘z) = v))
27		cleqcom 1103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((f ‘z) = v ↔ v = (f ‘z))
28	26, 27	syl6bb 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((f ‘t) = v → ((f ‘z) = (f ‘t) ↔ v = (f ‘z)))
29		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (z = t → (f ‘z) = (f ‘t))
30	28, 29	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((f ‘t) = v → (z = t → v = (f ‘z)))
31	30	ad2antrl 322	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) ∧ ((f ‘t) = v ∧ v ∈ z)) → (z = t → v = (f ‘z)))
32	25, 31	mpd 46	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) ∧ ((f ‘t) = v ∧ v ∈ z)) → v = (f ‘z))
33	32	exp32 294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((f ‘t) ∈ t ∧ (¬ z = t → (z ∩ t) = ∅)) → ((f ‘t) = v → (v ∈ z → v = (f ‘z))))
34	11, 33	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → (t ∈ x → ((f ‘t) = v → (v ∈ z → v = (f ‘z)))))
35	34	com14 38	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (v ∈ z → (t ∈ x → ((f ‘t) = v → (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → v = (f ‘z)))))
36	35	r19.23adv 1286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v ∈ z → (∃t ∈ x (f ‘t) = v → (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → v = (f ‘z))))
37		fvelrn 2883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f Fn x → (v ∈ ran f ↔ ∃t ∈ x (f ‘t) = v))
38	37	biimpac 326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((v ∈ ran f ∧ f Fn x) → ∃t ∈ x (f ‘t) = v)
39	36, 38	syl5 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (v ∈ z → ((v ∈ ran f ∧ f Fn x) → (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → v = (f ‘z))))
40	39	exp3a 292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (v ∈ z → (v ∈ ran f → (f Fn x → (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → v = (f ‘z)))))
41	40	com4t 40	. . . . . . . . . . . . . . . . . . . 20 ⊢ (f Fn x → (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) → (v ∈ z → (v ∈ ran f → v = (f ‘z)))))
42	41	imp4b 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((f Fn x ∧ ∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅))) → ((v ∈ z ∧ v ∈ ran f) → v = (f ‘z)))
43		elin 1635	. . . . . . . . . . . . . . . . . . 19 ⊢ (v ∈ (z ∩ ran f) ↔ (v ∈ z ∧ v ∈ ran f))
44	42, 43	syl5ib 181	. . . . . . . . . . . . . . . . . 18 ⊢ ((f Fn x ∧ ∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅))) → (v ∈ (z ∩ ran f) → v = (f ‘z)))
45		r19.26 1289	. . . . . . . . . . . . . . . . . 18 ⊢ (∀w ∈ x ((f ‘w) ∈ w ∧ (¬ z = w → (z ∩ w) = ∅)) ↔ (∀w ∈ x (f ‘w) ∈ w ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)))
46	44, 45	sylan2br 348	. . . . . . . . . . . . . . . . 17 ⊢ ((f Fn x ∧ (∀w ∈ x (f ‘w) ∈ w ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅))) → (v ∈ (z ∩ ran f) → v = (f ‘z)))
47	46	anassrs 338	. . . . . . . . . . . . . . . 16 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → (v ∈ (z ∩ ran f) → v = (f ‘z)))
48	47	adantlr 310	. . . . . . . . . . . . . . 15 ⊢ ((((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → (v ∈ (z ∩ ran f) → v = (f ‘z)))
49		eleq1 1149	. . . . . . . . . . . . . . . . . 18 ⊢ (v = (f ‘z) → (v ∈ (z ∩ ran f) ↔ (f ‘z) ∈ (z ∩ ran f)))
50		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = z → (f ‘w) = (f ‘z))
51		id 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (w = z → w = z)
52	50, 51	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (w = z → ((f ‘w) ∈ w ↔ (f ‘z) ∈ z))
53	52	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀w ∈ x (f ‘w) ∈ w → (z ∈ x → (f ‘z) ∈ z))
54	53	com12 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ x → (∀w ∈ x (f ‘w) ∈ w → (f ‘z) ∈ z))
55		fnfvrn 2889	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f Fn x ∧ z ∈ x) → (f ‘z) ∈ ran f)
56	55	exp 291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (f Fn x → (z ∈ x → (f ‘z) ∈ ran f))
57	56	com12 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (z ∈ x → (f Fn x → (f ‘z) ∈ ran f))
58	54, 57	anim12d 431	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (z ∈ x → ((∀w ∈ x (f ‘w) ∈ w ∧ f Fn x) → ((f ‘z) ∈ z ∧ (f ‘z) ∈ ran f)))
59		elin 1635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f ‘z) ∈ (z ∩ ran f) ↔ ((f ‘z) ∈ z ∧ (f ‘z) ∈ ran f))
60	58, 59	syl6ibr 186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ x → ((∀w ∈ x (f ‘w) ∈ w ∧ f Fn x) → (f ‘z) ∈ (z ∩ ran f)))
61	60	exp3a 292	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z ∈ x → (∀w ∈ x (f ‘w) ∈ w → (f Fn x → (f ‘z) ∈ (z ∩ ran f))))
62	61	com13 33	. . . . . . . . . . . . . . . . . . 19 ⊢ (f Fn x → (∀w ∈ x (f ‘w) ∈ w → (z ∈ x → (f ‘z) ∈ (z ∩ ran f))))
63	62	imp31 280	. . . . . . . . . . . . . . . . . 18 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → (f ‘z) ∈ (z ∩ ran f))
64	49, 63	syl5bir 184	. . . . . . . . . . . . . . . . 17 ⊢ (v = (f ‘z) → (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → v ∈ (z ∩ ran f)))
65	64	com12 13	. . . . . . . . . . . . . . . 16 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → (v = (f ‘z) → v ∈ (z ∩ ran f)))
66	65	adantr 306	. . . . . . . . . . . . . . 15 ⊢ ((((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → (v = (f ‘z) → v ∈ (z ∩ ran f)))
67	48, 66	impbid 397	. . . . . . . . . . . . . 14 ⊢ ((((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) ∧ ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → (v ∈ (z ∩ ran f) ↔ v = (f ‘z)))
68	67	exp 291	. . . . . . . . . . . . 13 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → (∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → (v ∈ (z ∩ ran f) ↔ v = (f ‘z))))
69	68	19.21adv 945	. . . . . . . . . . . 12 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → (∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∀v(v ∈ (z ∩ ran f) ↔ v = (f ‘z))))
70		fvex 2838	. . . . . . . . . . . . . 14 ⊢ (f ‘z) ∈ V
71		cleq2 1110	. . . . . . . . . . . . . . . 16 ⊢ (h = (f ‘z) → (v = h ↔ v = (f ‘z)))
72	71	bibi2d 470	. . . . . . . . . . . . . . 15 ⊢ (h = (f ‘z) → ((v ∈ (z ∩ ran f) ↔ v = h) ↔ (v ∈ (z ∩ ran f) ↔ v = (f ‘z))))
73	72	bialdv 935	. . . . . . . . . . . . . 14 ⊢ (h = (f ‘z) → (∀v(v ∈ (z ∩ ran f) ↔ v = h) ↔ ∀v(v ∈ (z ∩ ran f) ↔ v = (f ‘z))))
74	70, 73	cla4ev 1401	. . . . . . . . . . . . 13 ⊢ (∀v(v ∈ (z ∩ ran f) ↔ v = (f ‘z)) → ∃h∀v(v ∈ (z ∩ ran f) ↔ v = h))
75		df-eu 1009	. . . . . . . . . . . . 13 ⊢ (∃!v v ∈ (z ∩ ran f) ↔ ∃h∀v(v ∈ (z ∩ ran f) ↔ v = h))
76	74, 75	sylibr 175	. . . . . . . . . . . 12 ⊢ (∀v(v ∈ (z ∩ ran f) ↔ v = (f ‘z)) → ∃!v v ∈ (z ∩ ran f))
77	69, 76	syl6 23	. . . . . . . . . . 11 ⊢ (((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) ∧ z ∈ x) → (∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∃!v v ∈ (z ∩ ran f)))
78	77	r19.20dva 1256	. . . . . . . . . 10 ⊢ ((f Fn x ∧ ∀w ∈ x (f ‘w) ∈ w) → (∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∀z ∈ x ∃!v v ∈ (z ∩ ran f)))
79	78	exp 291	. . . . . . . . 9 ⊢ (f Fn x → (∀w ∈ x (f ‘w) ∈ w → (∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∀z ∈ x ∃!v v ∈ (z ∩ ran f))))
80		cleq1 1107	. . . . . . . . . . . . . 14 ⊢ (z = w → (z = ∅ ↔ w = ∅))
81	80	negbid 463	. . . . . . . . . . . . 13 ⊢ (z = w → (¬ z = ∅ ↔ ¬ w = ∅))
82	81	cbvralv 1333	. . . . . . . . . . . 12 ⊢ (∀z ∈ x ¬ z = ∅ ↔ ∀w ∈ x ¬ w = ∅)
83	82	anbi2i 367	. . . . . . . . . . 11 ⊢ ((∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀z ∈ x ¬ z = ∅) ↔ (∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀w ∈ x ¬ w = ∅))
84		r19.26 1289	. . . . . . . . . . 11 ⊢ (∀w ∈ x ((¬ w = ∅ → (f ‘w) ∈ w) ∧ ¬ w = ∅) ↔ (∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀w ∈ x ¬ w = ∅))
85	83, 84	bitr4 154	. . . . . . . . . 10 ⊢ ((∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀z ∈ x ¬ z = ∅) ↔ ∀w ∈ x ((¬ w = ∅ → (f ‘w) ∈ w) ∧ ¬ w = ∅))
86		pm3.35 278	. . . . . . . . . . . 12 ⊢ ((¬ w = ∅ ∧ (¬ w = ∅ → (f ‘w) ∈ w)) → (f ‘w) ∈ w)
87	86	ancoms 334	. . . . . . . . . . 11 ⊢ (((¬ w = ∅ → (f ‘w) ∈ w) ∧ ¬ w = ∅) → (f ‘w) ∈ w)
88	87	r19.20si 1254	. . . . . . . . . 10 ⊢ (∀w ∈ x ((¬ w = ∅ → (f ‘w) ∈ w) ∧ ¬ w = ∅) → ∀w ∈ x (f ‘w) ∈ w)
89	85, 88	sylbi 174	. . . . . . . . 9 ⊢ ((∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀z ∈ x ¬ z = ∅) → ∀w ∈ x (f ‘w) ∈ w)
90	79, 89	syl5 22	. . . . . . . 8 ⊢ (f Fn x → ((∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ∧ ∀z ∈ x ¬ z = ∅) → (∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∀z ∈ x ∃!v v ∈ (z ∩ ran f))))
91	90	exp3a 292	. . . . . . 7 ⊢ (f Fn x → (∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) → (∀z ∈ x ¬ z = ∅ → (∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅) → ∀z ∈ x ∃!v v ∈ (z ∩ ran f)))))
92	91	imp4b 283	. . . . . 6 ⊢ ((f Fn x ∧ ∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w)) → ((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∀z ∈ x ∃!v v ∈ (z ∩ ran f)))
93		visset 1350	. . . . . . . 8 ⊢ f ∈ V
94		rnexg 2569	. . . . . . . 8 ⊢ (f ∈ V → ran f ∈ V)
95	93, 94	ax-mp 6	. . . . . . 7 ⊢ ran f ∈ V
96		ineq2 1639	. . . . . . . . . 10 ⊢ (y = ran f → (z ∩ y) = (z ∩ ran f))
97	96	eleq2d 1156	. . . . . . . . 9 ⊢ (y = ran f → (v ∈ (z ∩ y) ↔ v ∈ (z ∩ ran f)))
98	97	bieudv 1013	. . . . . . . 8 ⊢ (y = ran f → (∃!v v ∈ (z ∩ y) ↔ ∃!v v ∈ (z ∩ ran f)))
99	98	biraldv 1219	. . . . . . 7 ⊢ (y = ran f → (∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∀z ∈ x ∃!v v ∈ (z ∩ ran f)))
100	95, 99	cla4ev 1401	. . . . . 6 ⊢ (∀z ∈ x ∃!v v ∈ (z ∩ ran f) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y))
101	92, 100	syl6 23	. . . . 5 ⊢ ((f Fn x ∧ ∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w)) → ((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
102	101	19.23aiv 952	. . . 4 ⊢ (∃f(f Fn x ∧ ∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w)) → ((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
103	102	19.20i 691	. . 3 ⊢ (∀x∃f(f Fn x ∧ ∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w)) → ∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
104	1, 103	sylbi 174	. 2 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) → ∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
105		cleqid 1102	. . . . 5 ⊢ {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))} = {u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))}
106		cleqid 1102	. . . . 5 ⊢ (∪{u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))} ∩ y) = (∪{u∣(¬ u = ∅ ∧ ∃t ∈ h u = ({t} × t))} ∩ y)
107		pm4.2 148	. . . . 5 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) ↔ ∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))
108	105, 106, 107	aceq5lem5 3562	. . . 4 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) → ∃f∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w))
109	108	19.21aiv 943	. . 3 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) → ∀h∃f∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w))
110		aceq3 3556	. . . 4 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) ↔ ∀x∃f∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w))
111		raleq 1324	. . . . . 6 ⊢ (x = h → (∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ↔ ∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w)))
112	111	biexdv 936	. . . . 5 ⊢ (x = h → (∃f∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ↔ ∃f∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w)))
113	112	cbvalv 972	. . . 4 ⊢ (∀x∃f∀w ∈ x (¬ w = ∅ → (f ‘w) ∈ w) ↔ ∀h∃f∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w))
114	110, 113	bitr2 152	. . 3 ⊢ (∀h∃f∀w ∈ h (¬ w = ∅ → (f ‘w) ∈ w) ↔ ∀x∃f(f ⊆ x ∧ f Fn dom x))
115	109, 114	sylib 173	. 2 ⊢ (∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)) → ∀x∃f(f ⊆ x ∧ f Fn dom x))
116	104, 115	impbi 139	1 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) ↔ ∀x((∀z ∈ x ¬ z = ∅ ∧ ∀z ∈ x ∀w ∈ x (¬ z = w → (z ∩ w) = ∅)) → ∃y∀z ∈ x ∃!v v ∈ (z ∩ y)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  ∃!weu 1007  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808  ∪cuni 1919   × cxp 2408  dom cdm 2410  ran crn 2411   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  ac8 3579  aceqkm 3596

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-fv 2438

metamath.org