HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem aceq6b 3565
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 3568). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, eirrv 3449 and preleq 3454 that are referenced in the proof each make use of Regularity for their derivations. (The reverse derivation can be done without using Regularity; see aceq6a 3564.)
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(s):   x,y,z,w,v,f
Proof of Theorem aceq6b
StepHypRef Expression
1 aceq3 3556 . 2 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) ↔ ∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z))
2 hbra1 1237 . . . . . 6 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∀z∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z))
3 ra4 1243 . . . . . . . . . . . 12 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → (z ∈ x → (¬ z = ∅ → (f ‘z) ∈ z)))
4 fvex 2838 . . . . . . . . . . . . . . 15 ⊢ (f ‘z) ∈ V
5 eleq1 1149 . . . . . . . . . . . . . . . 16 ⊢ (w = (f ‘z) → (w ∈ z ↔ (f ‘z) ∈ z))
6 eleq1 1149 . . . . . . . . . . . . . . . . . 18 ⊢ (w = (f ‘z) → (w ∈ v ↔ (f ‘z) ∈ v))
76anbi2d 468 . . . . . . . . . . . . . . . . 17 ⊢ (w = (f ‘z) → ((z ∈ v ∧ w ∈ v) ↔ (z ∈ v ∧ (f ‘z) ∈ v)))
87birexdv 1220 . . . . . . . . . . . . . . . 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 476 . . . . . . . . . . . . . . 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 1401 . . . . . . . . . . . . . 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 cleqid 1102 . . . . . . . . . . . . . . . . . . 19 ⊢ z = z
12 cleq1 1107 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (u = z → (u = ∅ ↔ z = ∅))
1312negbid 463 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → (¬ u = ∅ ↔ ¬ z = ∅))
14 cleq1 1107 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → (u = z ↔ z = z))
1513, 14anbi12d 476 . . . . . . . . . . . . . . . . . . . 20 ⊢ (u = z → ((¬ u = ∅ ∧ u = z) ↔ (¬ z = ∅ ∧ z = z)))
1615rcla4ev 1403 . . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ x ∧ (¬ z = ∅ ∧ z = z)) → ∃u ∈ x (¬ u = ∅ ∧ u = z))
1711, 16mpan22 532 . . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ x ∧ ¬ z = ∅) → ∃u ∈ x (¬ u = ∅ ∧ u = z))
18 fveq2 2832 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (u = z → (f ‘u) = (f ‘z))
19 preq1 1870 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((f ‘u) = (f ‘z) → {(f ‘u), u} = {(f ‘z), u})
2018, 19syl 12 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → {(f ‘u), u} = {(f ‘z), u})
21 preq2 1871 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u = z → {(f ‘z), u} = {(f ‘z), z})
2220, 21eqtr2d 1129 . . . . . . . . . . . . . . . . . . . 20 ⊢ (u = z → {(f ‘z), z} = {(f ‘u), u})
2322anim2i 270 . . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ u = ∅ ∧ u = z) → (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u}))
2423r19.22si 1275 . . . . . . . . . . . . . . . . . 18 ⊢ (∃u ∈ x (¬ u = ∅ ∧ u = z) → ∃u ∈ x (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u}))
2517, 24syl 12 . . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ x ∧ ¬ z = ∅) → ∃u ∈ x (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u}))
26 prex 1892 . . . . . . . . . . . . . . . . . 18 ⊢ {(f ‘z), z} ∈ V
27 cleq1 1107 . . . . . . . . . . . . . . . . . . . 20 ⊢ (g = {(f ‘z), z} → (g = {(f ‘u), u} ↔ {(f ‘z), z} = {(f ‘u), u}))
2827anbi2d 468 . . . . . . . . . . . . . . . . . . 19 ⊢ (g = {(f ‘z), z} → ((¬ u = ∅ ∧ g = {(f ‘u), u}) ↔ (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u})))
2928birexdv 1220 . . . . . . . . . . . . . . . . . 18 ⊢ (g = {(f ‘z), z} → (∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u}) ↔ ∃u ∈ x (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u})))
3026, 29elab 1415 . . . . . . . . . . . . . . . . 17 ⊢ ({(f ‘z), z} ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} ↔ ∃u ∈ x (¬ u = ∅ ∧ {(f ‘z), z} = {(f ‘u), u}))
3125, 30sylibr 175 . . . . . . . . . . . . . . . 16 ⊢ ((z ∈ x ∧ ¬ z = ∅) → {(f ‘z), z} ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})})
32 visset 1350 . . . . . . . . . . . . . . . . . 18 ⊢ z ∈ V
3332pri2 1842 . . . . . . . . . . . . . . . . 17 ⊢ z ∈ {(f ‘z), z}
344pri1 1841 . . . . . . . . . . . . . . . . 17 ⊢ (f ‘z) ∈ {(f ‘z), z}
3533, 34pm3.2i 234 . . . . . . . . . . . . . . . 16 ⊢ (z ∈ {(f ‘z), z} ∧ (f ‘z) ∈ {(f ‘z), z})
3631, 35jctir 241 . . . . . . . . . . . . . . 15 ⊢ ((z ∈ x ∧ ¬ z = ∅) → ({(f ‘z), z} ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} ∧ (z ∈ {(f ‘z), z} ∧ (f ‘z) ∈ {(f ‘z), z})))
37 eleq2 1150 . . . . . . . . . . . . . . . . 17 ⊢ (v = {(f ‘z), z} → (z ∈ v ↔ z ∈ {(f ‘z), z}))
38 eleq2 1150 . . . . . . . . . . . . . . . . 17 ⊢ (v = {(f ‘z), z} → ((f ‘z) ∈ v ↔ (f ‘z) ∈ {(f ‘z), z}))
3937, 38anbi12d 476 . . . . . . . . . . . . . . . 16 ⊢ (v = {(f ‘z), z} → ((z ∈ v ∧ (f ‘z) ∈ v) ↔ (z ∈ {(f ‘z), z} ∧ (f ‘z) ∈ {(f ‘z), z})))
4039rcla4ev 1403 . . . . . . . . . . . . . . 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))
4136, 40syl 12 . . . . . . . . . . . . . 14 ⊢ ((z ∈ x ∧ ¬ z = ∅) → ∃v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} (z ∈ v ∧ (f ‘z) ∈ v))
4210, 41sylan2 346 . . . . . . . . . . . . 13 ⊢ (((f ‘z) ∈ z ∧ (z ∈ x ∧ ¬ z = ∅)) → ∃w(w ∈ z ∧ ∃v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} (z ∈ v ∧ w ∈ v)))
4342exp 291 . . . . . . . . . . . 12 ⊢ ((f ‘z) ∈ z → ((z ∈ x ∧ ¬ z = ∅) → ∃w(w ∈ z ∧ ∃v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} (z ∈ v ∧ w ∈ v))))
443, 43syl8 25 . . . . . . . . . . 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))))))
4544imp3a 279 . . . . . . . . . 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)))))
4645pm2.43d 59 . . . . . . . . 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))))
47 visset 1350 . . . . . . . . . . . . . . . . . . . . 21 ⊢ v ∈ V
48 cleq1 1107 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (g = v → (g = {(f ‘u), u} ↔ v = {(f ‘u), u}))
4948anbi2d 468 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (g = v → ((¬ u = ∅ ∧ g = {(f ‘u), u}) ↔ (¬ u = ∅ ∧ v = {(f ‘u), u})))
5049birexdv 1220 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (g = v → (∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u}) ↔ ∃u ∈ x (¬ u = ∅ ∧ v = {(f ‘u), u})))
5147, 50elab 1415 . . . . . . . . . . . . . . . . . . . 20 ⊢ (v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} ↔ ∃u ∈ x (¬ u = ∅ ∧ v = {(f ‘u), u}))
52 cleq1 1107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = u → (z = ∅ ↔ u = ∅))
5352negbid 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (z = u → (¬ z = ∅ ↔ ¬ u = ∅))
54 fveq2 2832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (z = u → (f ‘z) = (f ‘u))
5554eleq1d 1155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = u → ((f ‘z) ∈ z ↔ (f ‘u) ∈ z))
56 eleq2 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (z = u → ((f ‘u) ∈ z ↔ (f ‘u) ∈ u))
5755, 56bitrd 406 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (z = u → ((f ‘z) ∈ z ↔ (f ‘u) ∈ u))
5853, 57imbi12d 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (z = u → ((¬ z = ∅ → (f ‘z) ∈ z) ↔ (¬ u = ∅ → (f ‘u) ∈ u)))
5958rcla4v 1402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → (u ∈ x → (¬ u = ∅ → (f ‘u) ∈ u)))
60 visset 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ w ∈ V
61 fvex 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (f ‘u) ∈ V
62 visset 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ u ∈ V
6360, 32, 61, 62prel12 1875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ w = z → ({w, z} = {(f ‘u), u} ↔ (w ∈ {(f ‘u), u} ∧ z ∈ {(f ‘u), u})))
64 eleq2 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (v = {(f ‘u), u} → (w ∈ v ↔ w ∈ {(f ‘u), u}))
65 eleq2 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (v = {(f ‘u), u} → (z ∈ v ↔ z ∈ {(f ‘u), u}))
6664, 65anbi12d 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (v = {(f ‘u), u} → ((w ∈ v ∧ z ∈ v) ↔ (w ∈ {(f ‘u), u} ∧ z ∈ {(f ‘u), u})))
67 ancom 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((w ∈ v ∧ z ∈ v) ↔ (z ∈ v ∧ w ∈ v))
6866, 67syl5rbbr 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (v = {(f ‘u), u} → ((w ∈ {(f ‘u), u} ∧ z ∈ {(f ‘u), u}) ↔ (z ∈ v ∧ w ∈ v)))
6963, 68sylan9bbr 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((v = {(f ‘u), u} ∧ ¬ w = z) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ∧ w ∈ v)))
70 eirrv 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ¬ w ∈ w
71 eleq2 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (w = z → (w ∈ w ↔ w ∈ z))
7270, 71mtbii 538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (w = z → ¬ w ∈ z)
7372con2i 89 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (w ∈ z → ¬ w = z)
7469, 73sylan2 346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((v = {(f ‘u), u} ∧ w ∈ z) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ∧ w ∈ v)))
7574adantrr 312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((v = {(f ‘u), u} ∧ (w ∈ z ∧ (f ‘u) ∈ u)) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ∧ w ∈ v)))
7675exp 291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (v = {(f ‘u), u} → ((w ∈ z ∧ (f ‘u) ∈ u) → ({w, z} = {(f ‘u), u} ↔ (z ∈ v ∧ w ∈ v))))
7776pm5.32d 491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (v = {(f ‘u), u} → (((w ∈ z ∧ (f ‘u) ∈ u) ∧ {w, z} = {(f ‘u), u}) ↔ ((w ∈ z ∧ (f ‘u) ∈ u) ∧ (z ∈ v ∧ w ∈ v))))
7860, 32, 61, 62preleq 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((w ∈ z ∧ (f ‘u) ∈ u) ∧ {w, z} = {(f ‘u), u}) → (w = (f ‘u) ∧ z = u))
7977, 78syl6bir 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (v = {(f ‘u), u} → (((w ∈ z ∧ (f ‘u) ∈ u) ∧ (z ∈ v ∧ w ∈ v)) → (w = (f ‘u) ∧ z = u)))
8054cleq2d 1112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (z = u → (w = (f ‘z) ↔ w = (f ‘u)))
8180biimparc 327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((w = (f ‘u) ∧ z = u) → w = (f ‘z))
8279, 81syl6 23 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (v = {(f ‘u), u} → (((w ∈ z ∧ (f ‘u) ∈ u) ∧ (z ∈ v ∧ w ∈ v)) → w = (f ‘z)))
8382exp4c 297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (v = {(f ‘u), u} → (w ∈ z → ((f ‘u) ∈ u → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))
8483com13 33 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((f ‘u) ∈ u → (w ∈ z → (v = {(f ‘u), u} → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))
8559, 84syl8 25 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → (u ∈ x → (¬ u = ∅ → (w ∈ z → (v = {(f ‘u), u} → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))))
8685com4r 41 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (w ∈ z → (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → (u ∈ x → (¬ u = ∅ → (v = {(f ‘u), u} → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))))
8786imp 277 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((w ∈ z ∧ ∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z)) → (u ∈ x → (¬ u = ∅ → (v = {(f ‘u), u} → ((z ∈ v ∧ w ∈ v) → w = (f ‘z))))))
8887imp4a 282 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w ∈ z ∧ ∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z)) → (u ∈ x → ((¬ u = ∅ ∧ v = {(f ‘u), u}) → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))
8988com3l 34 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (u ∈ x → ((¬ u = ∅ ∧ v = {(f ‘u), u}) → ((w ∈ z ∧ ∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z)) → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))
9089r19.23aiv 1284 . . . . . . . . . . . . . . . . . . . 20 ⊢ (∃u ∈ x (¬ u = ∅ ∧ v = {(f ‘u), u}) → ((w ∈ z ∧ ∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z)) → ((z ∈ v ∧ w ∈ v) → w = (f ‘z))))
9151, 90sylbi 174 . . . . . . . . . . . . . . . . . . 19 ⊢ (v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} → ((w ∈ z ∧ ∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z)) → ((z ∈ v ∧ w ∈ v) → w = (f ‘z))))
9291exp3a 292 . . . . . . . . . . . . . . . . . 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)))))
9392com13 33 . . . . . . . . . . . . . . . . 17 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → (w ∈ z → (v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} → ((z ∈ v ∧ w ∈ v) → w = (f ‘z)))))
9493imp4b 283 . . . . . . . . . . . . . . . 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)))
959419.23adv 954 . . . . . . . . . . . . . . 15 ⊢ ((∀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)))
96 df-rex 1206 . . . . . . . . . . . . . . 15 ⊢ (∃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)))
9795, 96syl5ib 181 . . . . . . . . . . . . . 14 ⊢ ((∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) ∧ w ∈ z) → (∃v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} (z ∈ v ∧ w ∈ v) → w = (f ‘z)))
9897exp 291 . . . . . . . . . . . . 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))))
9998imp3a 279 . . . . . . . . . . . 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)))
1009919.21aiv 943 . . . . . . . . . . 11 ⊢ (∀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)))
101 mo2icl 1434 . . . . . . . . . . 11 ⊢ (∀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)))
102100, 101syl 12 . . . . . . . . . 10 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃*w(w ∈ z ∧ ∃v ∈ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} (z ∈ v ∧ w ∈ v)))
103102a1d 14 . . . . . . . . 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))))
10446, 103jcad 455 . . . . . . . 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)))))
105 df-reu 1207 . . . . . . . . 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)))
106 eu5 1035 . . . . . . . . 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))))
107105, 106bitr 151 . . . . . . . 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))))
108104, 107syl6ibr 186 . . . . . . 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)))
109108exp3a 292 . . . . . 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))))
1102, 109r19.21ai 1258 . . . . 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)))
111 visset 1350 . . . . . . . 8 ⊢ x ∈ V
112111abrexex 2912 . . . . . . 7 ⊢ {g∣∃u ∈ x g = {(f ‘u), u}} ∈ V
113 pm3.27 260 . . . . . . . . 9 ⊢ ((¬ u = ∅ ∧ g = {(f ‘u), u}) → g = {(f ‘u), u})
114113r19.22si 1275 . . . . . . . 8 ⊢ (∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u}) → ∃u ∈ x g = {(f ‘u), u})
115114ss2abi 1552 . . . . . . 7 ⊢ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} ⊆ {g∣∃u ∈ x g = {(f ‘u), u}}
116112, 115ssexi 1701 . . . . . 6 ⊢ {g∣∃u ∈ x (¬ u = ∅ ∧ g = {(f ‘u), u})} ∈ V
117 rexeq 1325 . . . . . . . . 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)))
118117bireudv 1318 . . . . . . . 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)))
119118imbi2d 464 . . . . . . 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))))
120119biraldv 1219 . . . . . 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))))
121116, 120cla4ev 1401 . . . . 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)))
122110, 121syl 12 . . . 4 ⊢ (∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃y∀z ∈ x (¬ z = ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ∧ w ∈ v)))
12312219.23aiv 952 . . 3 ⊢ (∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∃y∀z ∈ x (¬ z = ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ∧ w ∈ v)))
12412319.20i 691 . 2 ⊢ (∀x∃f∀z ∈ x (¬ z = ∅ → (f ‘z) ∈ z) → ∀x∃y∀z ∈ x (¬ z = ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ∧ w ∈ v)))
1251, 124sylbi 174 1 ⊢ (∀x∃f(f ⊆ x ∧ f Fn dom x) → ∀x∃y∀z ∈ x (¬ z = ∅ → ∃!w ∈ z ∃v ∈ y (z ∈ v ∧ w ∈ v)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  ∃!weu 1007  ∃*wmo 1008  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  ∃!wreu 1203   ⊆ wss 1487  ∅c0 1707  {cpr 1809  dom cdm 2410   Fn wfn 2417   ‘cfv 2422
This theorem is referenced by:  aceq7 3566
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