HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem aceq6b 4722
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 4727). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 4578 and preleq 4583 that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see aceq6a 4721.)
Assertion
Ref Expression
aceq6b ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) → ∀x∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)))
Distinct variable group:   x,y,z,w,v,f
Proof of Theorem aceq6b
StepHypRef Expression
1 aceq3 4713 . 2 ⊢ (∀x∃f(f ⊆ x ⋀ f Fn dom x) ↔ ∀x∃f∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z))
2 hbra1 1684 . . . . . 6 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∀z∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z))
3 ra4 1691 . . . . . . . . . . . 12 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (z ∈ x → (z ≠ ∅ → (f ‘z) ∈ z)))
4 fvex 3723 . . . . . . . . . . . . . . 15 ⊢ (f ‘z) ∈ V
5 eleq1 1531 . . . . . . . . . . . . . . . 16 ⊢ (w = (f ‘z) → (w ∈ z ↔ (f ‘z) ∈ z))
6 eleq1 1531 . . . . . . . . . . . . . . . . . 18 ⊢ (w = (f ‘z) → (w ∈ v ↔ (f ‘z) ∈ v))
76anbi2d 615 . . . . . . . . . . . . . . . . 17 ⊢ (w = (f ‘z) → ((z ∈ v ⋀ w ∈ v) ↔ (z ∈ v ⋀ (f ‘z) ∈ v)))
87rexbidv 1661 . . . . . . . . . . . . . . . 16 ⊢ (w = (f ‘z) → (∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) ↔ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ (f ‘z) ∈ v)))
95, 8anbi12d 627 . . . . . . . . . . . . . . 15 ⊢ (w = (f ‘z) → ((w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) ↔ ((f ‘z) ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ (f ‘z) ∈ v))))
104, 9cla4ev 1865 . . . . . . . . . . . . . 14 ⊢ (((f ‘z) ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ (f ‘z) ∈ v)) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
11 eqid 1473 . . . . . . . . . . . . . . . . . . 19 ⊢ z = z
12 neeq1 1587 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → (u ≠ ∅ ↔ z ≠ ∅))
13 eqeq1 1478 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → (u = z ↔ z = z))
1412, 13anbi12d 627 . . . . . . . . . . . . . . . . . . . 20 ⊢ (u = z → ((u ≠ ∅ ⋀ u = z) ↔ (z ≠ ∅ ⋀ z = z)))
1514rcla4ev 1873 . . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ x ⋀ (z ≠ ∅ ⋀ z = z)) → ∃u ∈ x (u ≠ ∅ ⋀ u = z))
1611, 15mpanr2 709 . . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ x ⋀ z ≠ ∅) → ∃u ∈ x (u ≠ ∅ ⋀ u = z))
17 fveq2 3715 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (u = z → (f ‘u) = (f ‘z))
18 preq1 2444 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f ‘u) = (f ‘z) → {(f ‘u), u} = {(f ‘z), u})
1917, 18syl 10 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → {(f ‘u), u} = {(f ‘z), u})
20 preq2 2445 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → {(f ‘z), u} = {(f ‘z), z})
2119, 20eqtr2d 1505 . . . . . . . . . . . . . . . . . . . 20 ⊢ (u = z → {(f ‘z), z} = {(f ‘u), u})
2221anim2i 335 . . . . . . . . . . . . . . . . . . 19 ⊢ ((u ≠ ∅ ⋀ u = z) → (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u}))
2322r19.22si 1731 . . . . . . . . . . . . . . . . . 18 ⊢ (∃u ∈ x (u ≠ ∅ ⋀ u = z) → ∃u ∈ x (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u}))
2416, 23syl 10 . . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ x ⋀ z ≠ ∅) → ∃u ∈ x (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u}))
25 prex 2776 . . . . . . . . . . . . . . . . . 18 ⊢ {(f ‘z), z} ∈ V
26 eqeq1 1478 . . . . . . . . . . . . . . . . . . . 20 ⊢ (g = {(f ‘z), z} → (g = {(f ‘u), u} ↔ {(f ‘z), z} = {(f ‘u), u}))
2726anbi2d 615 . . . . . . . . . . . . . . . . . . 19 ⊢ (g = {(f ‘z), z} → ((u ≠ ∅ ⋀ g = {(f ‘u), u}) ↔ (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u})))
2827rexbidv 1661 . . . . . . . . . . . . . . . . . 18 ⊢ (g = {(f ‘z), z} → (∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u}) ↔ ∃u ∈ x (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u})))
2925, 28elab 1893 . . . . . . . . . . . . . . . . 17 ⊢ ({(f ‘z), z} ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ↔ ∃u ∈ x (u ≠ ∅ ⋀ {(f ‘z), z} = {(f ‘u), u}))
3024, 29sylibr 200 . . . . . . . . . . . . . . . 16 ⊢ ((z ∈ x ⋀ z ≠ ∅) → {(f ‘z), z} ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})})
31 visset 1809 . . . . . . . . . . . . . . . . . 18 ⊢ z ∈ V
3231pri2 2447 . . . . . . . . . . . . . . . . 17 ⊢ z ∈ {(f ‘z), z}
334pri1 2446 . . . . . . . . . . . . . . . . 17 ⊢ (f ‘z) ∈ {(f ‘z), z}
3432, 33pm3.2i 285 . . . . . . . . . . . . . . . 16 ⊢ (z ∈ {(f ‘z), z} ⋀ (f ‘z) ∈ {(f ‘z), z})
3530, 34jctir 293 . . . . . . . . . . . . . . 15 ⊢ ((z ∈ x ⋀ z ≠ ∅) → ({(f ‘z), z} ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⋀ (z ∈ {(f ‘z), z} ⋀ (f ‘z) ∈ {(f ‘z), z})))
36 eleq2 1532 . . . . . . . . . . . . . . . . 17 ⊢ (v = {(f ‘z), z} → (z ∈ v ↔ z ∈ {(f ‘z), z}))
37 eleq2 1532 . . . . . . . . . . . . . . . . 17 ⊢ (v = {(f ‘z), z} → ((f ‘z) ∈ v ↔ (f ‘z) ∈ {(f ‘z), z}))
3836, 37anbi12d 627 . . . . . . . . . . . . . . . 16 ⊢ (v = {(f ‘z), z} → ((z ∈ v ⋀ (f ‘z) ∈ v) ↔ (z ∈ {(f ‘z), z} ⋀ (f ‘z) ∈ {(f ‘z), z})))
3938rcla4ev 1873 . . . . . . . . . . . . . . 15 ⊢ (({(f ‘z), z} ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⋀ (z ∈ {(f ‘z), z} ⋀ (f ‘z) ∈ {(f ‘z), z})) → ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ (f ‘z) ∈ v))
4035, 39syl 10 . . . . . . . . . . . . . 14 ⊢ ((z ∈ x ⋀ z ≠ ∅) → ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ (f ‘z) ∈ v))
4110, 40sylan2 451 . . . . . . . . . . . . 13 ⊢ (((f ‘z) ∈ z ⋀ (z ∈ x ⋀ z ≠ ∅)) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
4241ex 373 . . . . . . . . . . . 12 ⊢ ((f ‘z) ∈ z → ((z ∈ x ⋀ z ≠ ∅) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
433, 42syl8 24 . . . . . . . . . . 11 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (z ∈ x → (z ≠ ∅ → ((z ∈ x ⋀ z ≠ ∅) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))))
4443imp3a 361 . . . . . . . . . 10 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((z ∈ x ⋀ z ≠ ∅) → ((z ∈ x ⋀ z ≠ ∅) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))))
4544pm2.43d 65 . . . . . . . . 9 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((z ∈ x ⋀ z ≠ ∅) → ∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
46 visset 1809 . . . . . . . . . . . . . . . . . . . 20 ⊢ v ∈ V
47 eqeq1 1478 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (g = v → (g = {(f ‘u), u} ↔ v = {(f ‘u), u}))
4847anbi2d 615 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (g = v → ((u ≠ ∅ ⋀ g = {(f ‘u), u}) ↔ (u ≠ ∅ ⋀ v = {(f ‘u), u})))
4948rexbidv 1661 . . . . . . . . . . . . . . . . . . . 20 ⊢ (g = v → (∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u}) ↔ ∃u ∈ x (u ≠ ∅ ⋀ v = {(f ‘u), u})))
5046, 49elab 1893 . . . . . . . . . . . . . . . . . . 19 ⊢ (v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ↔ ∃u ∈ x (u ≠ ∅ ⋀ v = {(f ‘u), u}))
51 neeq1 1587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (z = u → (z ≠ ∅ ↔ u ≠ ∅))
52 fveq2 3715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = u → (f ‘z) = (f ‘u))
5352eleq1d 1537 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (z = u → ((f ‘z) ∈ z ↔ (f ‘u) ∈ z))
54 eleq2 1532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (z = u → ((f ‘u) ∈ z ↔ (f ‘u) ∈ u))
5553, 54bitrd 527 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (z = u → ((f ‘z) ∈ z ↔ (f ‘u) ∈ u))
5651, 55imbi12d 625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (z = u → ((z ≠ ∅ → (f ‘z) ∈ z) ↔ (u ≠ ∅ → (f ‘u) ∈ u)))
5756rcla4cv 1870 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (u ∈ x → (u ≠ ∅ → (f ‘u) ∈ u)))
58 visset 1809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ w ∈ V
59 fvex 3723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (f ‘u) ∈ V
60 visset 1809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ u ∈ V
6158, 31, 59, 60prel12 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (¬ w = z → ({w, z} = {(f ‘u), u} ↔ (w ∈ {(f ‘u), u} ⋀ z ∈ {(f ‘u), u})))
62 eleq2 1532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (v = {(f ‘u), u} → (w ∈ v ↔ w ∈ {(f ‘u), u}))
63 eleq2 1532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (v = {(f ‘u), u} → (z ∈ v ↔ z ∈ {(f ‘u), u}))
6462, 63anbi12d 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (v = {(f ‘u), u} → ((w ∈ v ⋀ z ∈ v) ↔ (w ∈ {(f ‘u), u} ⋀ z ∈ {(f ‘u), u})))
65 ancom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((w ∈ v ⋀ z ∈ v) ↔ (z ∈ v ⋀ w ∈ v))
6664, 65syl5rbbr 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (v = {(f ‘u), u} → ((w ∈ {(f ‘u), u} ⋀ z ∈ {(f ‘u), u}) ↔ (z ∈ v ⋀ w ∈ v)))
6761, 66sylan9bbr 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((v = {(f ‘u), u} ⋀ ¬ w = z) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ⋀ w ∈ v)))
68 elirrv 4578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ¬ w ∈ w
69 eleq2 1532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (w = z → (w ∈ w ↔ w ∈ z))
7068, 69mtbii 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (w = z → ¬ w ∈ z)
7170con2i 97 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (w ∈ z → ¬ w = z)
7267, 71sylan2 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((v = {(f ‘u), u} ⋀ w ∈ z) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ⋀ w ∈ v)))
7372adantrr 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((v = {(f ‘u), u} ⋀ (w ∈ z ⋀ (f ‘u) ∈ u)) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ⋀ w ∈ v)))
7473pm5.32da 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (v = {(f ‘u), u} → (((w ∈ z ⋀ (f ‘u) ∈ u) ⋀ {w, z} = {(f ‘u), u}) ↔ ((w ∈ z ⋀ (f ‘u) ∈ u) ⋀ (z ∈ v ⋀ w ∈ v))))
7558, 31, 59, 60preleq 4583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((w ∈ z ⋀ (f ‘u) ∈ u) ⋀ {w, z} = {(f ‘u), u}) → (w = (f ‘u) ⋀ z = u))
7674, 75syl6bir 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v = {(f ‘u), u} → (((w ∈ z ⋀ (f ‘u) ∈ u) ⋀ (z ∈ v ⋀ w ∈ v)) → (w = (f ‘u) ⋀ z = u)))
7752eqeq2d 1483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = u → (w = (f ‘z) ↔ w = (f ‘u)))
7877biimparc 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((w = (f ‘u) ⋀ z = u) → w = (f ‘z))
7976, 78syl6 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v = {(f ‘u), u} → (((w ∈ z ⋀ (f ‘u) ∈ u) ⋀ (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)))
8079exp4c 380 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (v = {(f ‘u), u} → (w ∈ z → ((f ‘u) ∈ u → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
8180com13 33 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((f ‘u) ∈ u → (w ∈ z → (v = {(f ‘u), u} → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
8257, 81syl8 24 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (u ∈ x → (u ≠ ∅ → (w ∈ z → (v = {(f ‘u), u} → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))))
8382com4r 41 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (w ∈ z → (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (u ∈ x → (u ≠ ∅ → (v = {(f ‘u), u} → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))))
8483imp 350 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w ∈ z ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) → (u ∈ x → (u ≠ ∅ → (v = {(f ‘u), u} → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z))))))
8584imp4a 364 . . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ∈ z ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) → (u ∈ x → ((u ≠ ∅ ⋀ v = {(f ‘u), u}) → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
8685com3l 34 . . . . . . . . . . . . . . . . . . . 20 ⊢ (u ∈ x → ((u ≠ ∅ ⋀ v = {(f ‘u), u}) → ((w ∈ z ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
8786r19.23aiv 1740 . . . . . . . . . . . . . . . . . . 19 ⊢ (∃u ∈ x (u ≠ ∅ ⋀ v = {(f ‘u), u}) → ((w ∈ z ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z))))
8850, 87sylbi 199 . . . . . . . . . . . . . . . . . 18 ⊢ (v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → ((w ∈ z ⋀ ∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z)) → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z))))
8988exp3a 375 . . . . . . . . . . . . . . . . 17 ⊢ (v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → (w ∈ z → (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
9089com13 33 . . . . . . . . . . . . . . . 16 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (w ∈ z → (v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → ((z ∈ v ⋀ w ∈ v) → w = (f ‘z)))))
9190imp4b 365 . . . . . . . . . . . . . . 15 ⊢ ((∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) ⋀ w ∈ z) → ((v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⋀ (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)))
929119.23adv 1212 . . . . . . . . . . . . . 14 ⊢ ((∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) ⋀ w ∈ z) → (∃v(v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⋀ (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)))
93 df-rex 1647 . . . . . . . . . . . . . 14 ⊢ (∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) ↔ ∃v(v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⋀ (z ∈ v ⋀ w ∈ v)))
9492, 93syl5ib 206 . . . . . . . . . . . . 13 ⊢ ((∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) ⋀ w ∈ z) → (∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) → w = (f ‘z)))
9594ex 373 . . . . . . . . . . . 12 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (w ∈ z → (∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) → w = (f ‘z))))
9695imp3a 361 . . . . . . . . . . 11 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)))
979619.21aiv 1284 . . . . . . . . . 10 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∀w((w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)))
98 mo2icl 1919 . . . . . . . . . 10 ⊢ (∀w((w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) → w = (f ‘z)) → ∃*w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
9997, 98syl 10 . . . . . . . . 9 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∃*w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
10045, 99jctird 601 . . . . . . . 8 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((z ∈ x ⋀ z ≠ ∅) → (∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) ⋀ ∃*w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))))
101 df-reu 1648 . . . . . . . . 9 ⊢ (∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) ↔ ∃!w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
102 eu5 1407 . . . . . . . . 9 ⊢ (∃!w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) ↔ (∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) ⋀ ∃*w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
103101, 102bitr 173 . . . . . . . 8 ⊢ (∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v) ↔ (∃w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) ⋀ ∃*w(w ∈ z ⋀ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
104100, 103syl6ibr 213 . . . . . . 7 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ((z ∈ x ⋀ z ≠ ∅) → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
105104exp3a 375 . . . . . 6 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → (z ∈ x → (z ≠ ∅ → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
1062, 105r19.21ai 1709 . . . . 5 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
107 visset 1809 . . . . . . . 8 ⊢ x ∈ V
108107abrexex 3851 . . . . . . 7 ⊢ {g∣∃u ∈ x g = {(f ‘u), u}} ∈ V
109 pm3.27 323 . . . . . . . . 9 ⊢ ((u ≠ ∅ ⋀ g = {(f ‘u), u}) → g = {(f ‘u), u})
110109r19.22si 1731 . . . . . . . 8 ⊢ (∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u}) → ∃u ∈ x g = {(f ‘u), u})
111110ss2abi 2116 . . . . . . 7 ⊢ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ⊆ {g∣∃u ∈ x g = {(f ‘u), u}}
112108, 111ssexi 2715 . . . . . 6 ⊢ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} ∈ V
113 rexeq1 1784 . . . . . . . . 9 ⊢ (y = {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → (∃v ∈ y (z ∈ v ⋀ w ∈ v) ↔ ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
114113reubidv 1777 . . . . . . . 8 ⊢ (y = {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → (∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v) ↔ ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)))
115114imbi2d 611 . . . . . . 7 ⊢ (y = {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → ((z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)) ↔ (z ≠ ∅ → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
116115ralbidv 1660 . . . . . 6 ⊢ (y = {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} → (∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)) ↔ ∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v))))
117112, 116cla4ev 1865 . . . . 5 ⊢ (∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ {g∣∃u ∈ x (u ≠ ∅ ⋀ g = {(f ‘u), u})} (z ∈ v ⋀ w ∈ v)) → ∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)))
118106, 117syl 10 . . . 4 ⊢ (∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)))
11911819.23aiv 1293 . . 3 ⊢ (∃f∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)))
12011919.20i 990 . 2 ⊢ (∀x∃f∀z ∈ x (z ≠ ∅ → (f ‘z) ∈ z) → ∀x∃y∀z ∈ x (z ≠ ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ⋀ w ∈ v)))
1211, 120sylbi 199 1 ⊢ (∀x∃f(f ⊆