HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem ac6sfi 4591
Description: A version of ac6s 4902 for finite sets. (Contributed by Jeffrey Hankins, 26-Jun-2009.)
Hypothesis
Ref Expression
ac6sfi.1 ⊢ (y = (f ‘x) → (φ ↔ ψ))
Assertion
Ref Expression
ac6sfi ⊢ ((A ∈ Fin ⋀ ∀x ∈ A ∃y ∈ B φ) → ∃f(f:A–→B ⋀ ∀x ∈ A ψ))
Distinct variable groups:   x,f,A   y,f,B,x   φ,f   ψ,y
Proof of Theorem ac6sfi
StepHypRef Expression
1 isfi 4523 . . 3 ⊢ (A ∈ Fin ↔ ∃m ∈ ω A ≈ m)
2 relen 4513 . . . . . . 7 ⊢ Rel ≈
32brrelexi 3291 . . . . . 6 ⊢ (A ≈ m → A ∈ V)
4 visset 1859 . . . . . . . 8 ⊢ m ∈ V
54bren 4518 . . . . . . 7 ⊢ (A ≈ m ↔ ∃h h:A–1-1-onto→m)
6 f1oeq2 3793 . . . . . . . . . . . 12 ⊢ (z = A → (h:z–1-1-onto→m ↔ h:A–1-1-onto→m))
76exbidv 1317 . . . . . . . . . . 11 ⊢ (z = A → (∃h h:z–1-1-onto→m ↔ ∃h h:A–1-1-onto→m))
8 raleq1 1832 . . . . . . . . . . . 12 ⊢ (z = A → (∀x ∈ z ∃y ∈ B φ ↔ ∀x ∈ A ∃y ∈ B φ))
9 feq2 3728 . . . . . . . . . . . . . 14 ⊢ (z = A → (f:z–→B ↔ f:A–→B))
10 raleq1 1832 . . . . . . . . . . . . . 14 ⊢ (z = A → (∀x ∈ z ψ ↔ ∀x ∈ A ψ))
119, 10anbi12d 631 . . . . . . . . . . . . 13 ⊢ (z = A → ((f:z–→B ⋀ ∀x ∈ z ψ) ↔ (f:A–→B ⋀ ∀x ∈ A ψ)))
1211exbidv 1317 . . . . . . . . . . . 12 ⊢ (z = A → (∃f(f:z–→B ⋀ ∀x ∈ z ψ) ↔ ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))
138, 12imbi12d 629 . . . . . . . . . . 11 ⊢ (z = A → ((∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)) ↔ (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ))))
147, 13imbi12d 629 . . . . . . . . . 10 ⊢ (z = A → ((∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ (∃h h:A–1-1-onto→m → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))))
1514cla4gv 1908 . . . . . . . . 9 ⊢ (A ∈ V → (∀z(∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) → (∃h h:A–1-1-onto→m → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))))
16 f1oeq3 3794 . . . . . . . . . . . . 13 ⊢ (m = ∅ → (h:z–1-1-onto→m ↔ h:z–1-1-onto→∅))
1716exbidv 1317 . . . . . . . . . . . 12 ⊢ (m = ∅ → (∃h h:z–1-1-onto→m ↔ ∃h h:z–1-1-onto→∅))
1817imbi1d 616 . . . . . . . . . . 11 ⊢ (m = ∅ → ((∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ (∃h h:z–1-1-onto→∅ → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
1918albidv 1316 . . . . . . . . . 10 ⊢ (m = ∅ → (∀z(∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ ∀z(∃h h:z–1-1-onto→∅ → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
20 f1oeq3 3794 . . . . . . . . . . . . 13 ⊢ (m = w → (h:z–1-1-onto→m ↔ h:z–1-1-onto→w))
2120exbidv 1317 . . . . . . . . . . . 12 ⊢ (m = w → (∃h h:z–1-1-onto→m ↔ ∃h h:z–1-1-onto→w))
2221imbi1d 616 . . . . . . . . . . 11 ⊢ (m = w → ((∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ (∃h h:z–1-1-onto→w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
2322albidv 1316 . . . . . . . . . 10 ⊢ (m = w → (∀z(∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ ∀z(∃h h:z–1-1-onto→w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
24 f1oeq3 3794 . . . . . . . . . . . . 13 ⊢ (m = suc w → (h:z–1-1-onto→m ↔ h:z–1-1-onto→suc w))
2524exbidv 1317 . . . . . . . . . . . 12 ⊢ (m = suc w → (∃h h:z–1-1-onto→m ↔ ∃h h:z–1-1-onto→suc w))
2625imbi1d 616 . . . . . . . . . . 11 ⊢ (m = suc w → ((∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ (∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
2726albidv 1316 . . . . . . . . . 10 ⊢ (m = suc w → (∀z(∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ ∀z(∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
28 f1ocnv 3809 . . . . . . . . . . . . . 14 ⊢ (h:z–1-1-onto→∅ → ◡h:∅–1-1-onto→z)
29 f1o00 3825 . . . . . . . . . . . . . . 15 ⊢ (◡h:∅–1-1-onto→z ↔ (◡h = ∅ ⋀ z = ∅))
3029biimpi 149 . . . . . . . . . . . . . 14 ⊢ (◡h:∅–1-1-onto→z → (◡h = ∅ ⋀ z = ∅))
31 ax-17 1007 . . . . . . . . . . . . . . . 16 ⊢ (x ∈ ∅ → ∀f x ∈ ∅)
32 ax-17 1007 . . . . . . . . . . . . . . . . 17 ⊢ (∅:z–→B → ∀f∅:z–→B)
33 ax-17 1007 . . . . . . . . . . . . . . . . . 18 ⊢ (x ∈ z → ∀f x ∈ z)
34 0ex 2785 . . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ V
3534hbsbc1v 1995 . . . . . . . . . . . . . . . . . 18 ⊢ ([∅ / f]ψ → ∀f[∅ / f]ψ)
3633, 35hbral 1732 . . . . . . . . . . . . . . . . 17 ⊢ (∀x ∈ z [∅ / f]ψ → ∀f∀x ∈ z [∅ / f]ψ)
3732, 36hban 1045 . . . . . . . . . . . . . . . 16 ⊢ ((∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ) → ∀f(∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ))
38 feq1 3727 . . . . . . . . . . . . . . . . 17 ⊢ (f = ∅ → (f:z–→B ↔ ∅:z–→B))
39 sbceq1a 1989 . . . . . . . . . . . . . . . . . 18 ⊢ (f = ∅ → (ψ ↔ [∅ / f]ψ))
4039ralbidv 1709 . . . . . . . . . . . . . . . . 17 ⊢ (f = ∅ → (∀x ∈ z ψ ↔ ∀x ∈ z [∅ / f]ψ))
4138, 40anbi12d 631 . . . . . . . . . . . . . . . 16 ⊢ (f = ∅ → ((f:z–→B ⋀ ∀x ∈ z ψ) ↔ (∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ)))
4231, 37, 41cla4egf 1907 . . . . . . . . . . . . . . 15 ⊢ (∅ ∈ V → ((∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
4334a1i 8 . . . . . . . . . . . . . . 15 ⊢ ((◡h = ∅ ⋀ z = ∅) → ∅ ∈ V)
44 f0 3763 . . . . . . . . . . . . . . . . . 18 ⊢ ∅:∅–→B
45 ral0 2412 . . . . . . . . . . . . . . . . . 18 ⊢ ∀x ∈ ∅ [∅ / f]ψ
4644, 45pm3.2i 283 . . . . . . . . . . . . . . . . 17 ⊢ (∅:∅–→B ⋀ ∀x ∈ ∅ [∅ / f]ψ)
47 feq2 3728 . . . . . . . . . . . . . . . . . 18 ⊢ (z = ∅ → (∅:z–→B ↔ ∅:∅–→B))
48 raleq1 1832 . . . . . . . . . . . . . . . . . 18 ⊢ (z = ∅ → (∀x ∈ z [∅ / f]ψ ↔ ∀x ∈ ∅ [∅ / f]ψ))
4947, 48anbi12d 631 . . . . . . . . . . . . . . . . 17 ⊢ (z = ∅ → ((∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ) ↔ (∅:∅–→B ⋀ ∀x ∈ ∅ [∅ / f]ψ)))
5046, 49mpbiri 192 . . . . . . . . . . . . . . . 16 ⊢ (z = ∅ → (∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ))
5150adantl 388 . . . . . . . . . . . . . . 15 ⊢ ((◡h = ∅ ⋀ z = ∅) → (∅:z–→B ⋀ ∀x ∈ z [∅ / f]ψ))
5242, 43, 51sylc 68 . . . . . . . . . . . . . 14 ⊢ ((◡h = ∅ ⋀ z = ∅) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))
5328, 30, 523syl 20 . . . . . . . . . . . . 13 ⊢ (h:z–1-1-onto→∅ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))
5453a1d 12 . . . . . . . . . . . 12 ⊢ (h:z–1-1-onto→∅ → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
555419.23aiv 1333 . . . . . . . . . . 11 ⊢ (∃h h:z–1-1-onto→∅ → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
5655ax-gen 999 . . . . . . . . . 10 ⊢ ∀z(∃h h:z–1-1-onto→∅ → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
57 f1ores 3811 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((◡h:suc w–1-1→z ⋀ w ⊆ suc w) → (◡h ↾ w):w–1-1-onto→(◡h “ w))
58 f1of1 3796 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (◡h:suc w–1-1-onto→z → ◡h:suc w–1-1→z)
59 sssucid 3050 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ w ⊆ suc w
6059a1i 8 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (◡h:suc w–1-1-onto→z → w ⊆ suc w)
6157, 58, 60sylanc 473 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡h:suc w–1-1-onto→z → (◡h ↾ w):w–1-1-onto→(◡h “ w))
6261adantl 388 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((w ∈ ω ⋀ ◡h:suc w–1-1-onto→z) → (◡h ↾ w):w–1-1-onto→(◡h “ w))
63 f1ocnv 3809 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (h:z–1-1-onto→suc w → ◡h:suc w–1-1-onto→z)
6462, 63sylan2 453 . . . . . . . . . . . . . . . . . . . . 21 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (◡h ↾ w):w–1-1-onto→(◡h “ w))
65 f1ocnv 3809 . . . . . . . . . . . . . . . . . . . . 21 ⊢ ((◡h ↾ w):w–1-1-onto→(◡h “ w) → ◡(◡h ↾ w):(◡h “ w)–1-1-onto→w)
66 visset 1859 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ h ∈ V
6766cnvex 3625 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ◡h ∈ V
68 resexg 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (◡h ∈ V → (◡h ↾ w) ∈ V)
6967, 68ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (◡h ↾ w) ∈ V
7069cnvex 3625 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ◡(◡h ↾ w) ∈ V
71 f1oeq1 3792 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (k = ◡(◡h ↾ w) → (k:(◡h “ w)–1-1-onto→w ↔ ◡(◡h ↾ w):(◡h “ w)–1-1-onto→w))
7270, 71cla4ev 1915 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡(◡h ↾ w):(◡h “ w)–1-1-onto→w → ∃k k:(◡h “ w)–1-1-onto→w)
7364, 65, 723syl 20 . . . . . . . . . . . . . . . . . . . 20 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → ∃k k:(◡h “ w)–1-1-onto→w)
74 pm2.27 62 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃k k:(◡h “ w)–1-1-onto→w → ((∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))) → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))))
75 dff1o5 3805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡h:suc w–1-1-onto→z ↔ (◡h:suc w–1-1→z ⋀ ran ◡ h = z))
7675biimpi 149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (◡h:suc w–1-1-onto→z → (◡h:suc w–1-1→z ⋀ ran ◡ h = z))
77 pm3.27 321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((◡h:suc w–1-1→z ⋀ ran ◡ h = z) → ran ◡ h = z)
78 imassrn 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (◡h “ w) ⊆ ran ◡ h
79 sseq2 2135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (ran ◡ h = z → ((◡h “ w) ⊆ ran ◡ h ↔ (◡h “ w) ⊆ z))
8078, 79mpbii 191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (ran ◡ h = z → (◡h “ w) ⊆ z)
8176, 77, 803syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (◡h:suc w–1-1-onto→z → (◡h “ w) ⊆ z)
82 ssralv 2166 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((◡h “ w) ⊆ z → (∀x ∈ z ∃y ∈ B φ → ∀x ∈ (◡h “ w)∃y ∈ B φ))
8363, 81, 823syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∀x ∈ (◡h “ w)∃y ∈ B φ))
8483adantl 388 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∀x ∈ z ∃y ∈ B φ → ∀x ∈ (◡h “ w)∃y ∈ B φ))
8584imp 348 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∀x ∈ (◡h “ w)∃y ∈ B φ)
86 pm2.27 62 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∀x ∈ (◡h “ w)∃y ∈ B φ → ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)))
87 ax-17 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ) → ∀g(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))
88 ax-17 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (g:(◡h “ w)–→B → ∀f g:(◡h “ w)–→B)
89 ax-17 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (x ∈ (◡h “ w) → ∀f x ∈ (◡h “ w))
90 visset 1859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ g ∈ V
9190hbsbc1v 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ([g / f]ψ → ∀f[g / f]ψ)
9289, 91hbral 1732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∀x ∈ (◡h “ w)[g / f]ψ → ∀f∀x ∈ (◡h “ w)[g / f]ψ)
9388, 92hban 1045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∀f(g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ))
94 feq1 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f = g → (f:(◡h “ w)–→B ↔ g:(◡h “ w)–→B))
95 sbequ12 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (f = g → (ψ ↔ [g / f]ψ))
9695ralbidv 1709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (f = g → (∀x ∈ (◡h “ w)ψ ↔ ∀x ∈ (◡h “ w)[g / f]ψ))
9794, 96anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (f = g → ((f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ) ↔ (g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ)))
9887, 93, 97cbvex 1203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ) ↔ ∃g(g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ))
99 ssralv 2166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ({(◡h ‘w)} ⊆ z → (∀x ∈ z ∃y ∈ B φ → ∀x ∈ {(◡h ‘w)}∃y ∈ B φ))
10099imp 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (({(◡h ‘w)} ⊆ z ⋀ ∀x ∈ z ∃y ∈ B φ) → ∀x ∈ {(◡h ‘w)}∃y ∈ B φ)
101 visset 1859 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ w ∈ V
102101sucid 3051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ w ∈ suc w
103 fnsnfv 3878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((◡h Fn suc w ⋀ w ∈ suc w) → {(◡h ‘w)} = (◡h “ {w}))
104102, 103mpan2 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (◡h Fn suc w → {(◡h ‘w)} = (◡h “ {w}))
105104eqcomd 1523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (◡h Fn suc w → (◡h “ {w}) = {(◡h ‘w)})
106105sseq1d 2140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡h Fn suc w → ((◡h “ {w}) ⊆ z ↔ {(◡h ‘w)} ⊆ z))
107106biimpa 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((◡h Fn suc w ⋀ (◡h “ {w}) ⊆ z) → {(◡h ‘w)} ⊆ z)
108100, 107sylan 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((◡h Fn suc w ⋀ (◡h “ {w}) ⊆ z) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∀x ∈ {(◡h ‘w)}∃y ∈ B φ)
109 f1ofo 3803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡h:suc w–1-1-onto→z → ◡h:suc w–onto→z)
110 fofn 3781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡h:suc w–onto→z → ◡h Fn suc w)
11163, 109, 1103syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (h:z–1-1-onto→suc w → ◡h Fn suc w)
112 foima 3784 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (◡h:suc w–onto→z → (◡h “ suc w) = z)
11363, 109, 1123syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (h:z–1-1-onto→suc w → (◡h “ suc w) = z)
114 df-suc 2981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ suc w = (w ∪ {w})
115114imaeq2i 3494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (◡h “ suc w) = (◡h “ (w ∪ {w}))
116 imaundi 3545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (◡h “ (w ∪ {w})) = ((◡h “ w) ∪ (◡h “ {w}))
117115, 116eqtri 1538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (◡h “ suc w) = ((◡h “ w) ∪ (◡h “ {w}))
118117eqeq1i 1525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((◡h “ suc w) = z ↔ ((◡h “ w) ∪ (◡h “ {w})) = z)
119118biimpi 149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((◡h “ suc w) = z → ((◡h “ w) ∪ (◡h “ {w})) = z)
120 ssun2 2246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (◡h “ {w}) ⊆ ((◡h “ w) ∪ (◡h “ {w}))
121 sseq2 2135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((◡h “ w) ∪ (◡h “ {w})) = z → ((◡h “ {w}) ⊆ ((◡h “ w) ∪ (◡h “ {w})) ↔ (◡h “ {w}) ⊆ z))
122120, 121mpbii 191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((◡h “ w) ∪ (◡h “ {w})) = z → (◡h “ {w}) ⊆ z)
123113, 119, 1223syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (h:z–1-1-onto→suc w → (◡h “ {w}) ⊆ z)
124111, 123jca 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (h:z–1-1-onto→suc w → (◡h Fn suc w ⋀ (◡h “ {w}) ⊆ z))
125108, 124sylan 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((h:z–1-1-onto→suc w ⋀ ∀x ∈ z ∃y ∈ B φ) → ∀x ∈ {(◡h ‘w)}∃y ∈ B φ)
126125adantll 392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∀x ∈ {(◡h ‘w)}∃y ∈ B φ)
127 ac6sfi.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (y = (f ‘x) → (φ ↔ ψ))
128127ac6sfilem3 4590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((y ∈ B ⋀ [(◡h ‘w) / x]φ ⋀ (w ∈ ω ⋀ ◡h:suc w–1-1-onto→z)) ⋀ (g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ)) → ((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ))
129 snex 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ {<.(◡h ‘w), y>.} ∈ V
13090, 129unex 3095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (g ∪ {<.(◡h ‘w), y>.}) ∈ V
131 ax-17 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (t ∈ (g ∪ {<.(◡h ‘w), y>.}) → ∀f t ∈ (g ∪ {<.(◡h ‘w), y>.}))
132 ax-17 1007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((g ∪ {<.(◡h ‘w), y>.}):z–→B → ∀f(g ∪ {<.(◡h ‘w), y>.}):z–→B)
133130hbsbc1v 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ([(g ∪ {<.(◡h ‘w), y>.}) / f]ψ → ∀f[(g ∪ {<.(◡h ‘w), y>.}) / f]ψ)
13433, 133hbral 1732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ → ∀f∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ)
135132, 134hban 1045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ) → ∀f((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ))
136 feq1 3727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (f = (g ∪ {<.(◡h ‘w), y>.}) → (f:z–→B ↔ (g ∪ {<.(◡h ‘w), y>.}):z–→B))
137 sbceq1a 1989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (f = (g ∪ {<.(◡h ‘w), y>.}) → (ψ ↔ [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ))
138137ralbidv 1709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (f = (g ∪ {<.(◡h ‘w), y>.}) → (∀x ∈ z ψ ↔ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ))
139136, 138anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (f = (g ∪ {<.(◡h ‘w), y>.}) → ((f:z–→B ⋀ ∀x ∈ z ψ) ↔ ((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ)))
140131, 135, 139cla4egf 1907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((g ∪ {<.(◡h ‘w), y>.}) ∈ V → (((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
141130, 140ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((g ∪ {<.(◡h ‘w), y>.}):z–→B ⋀ ∀x ∈ z [(g ∪ {<.(◡h ‘w), y>.}) / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))
142128, 141syl 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((y ∈ B ⋀ [(◡h ‘w) / x]φ ⋀ (w ∈ ω ⋀ ◡h:suc w–1-1-onto→z)) ⋀ (g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ)) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))
1431423exp1 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (y ∈ B → ([(◡h ‘w) / x]φ → ((w ∈ ω ⋀ ◡h:suc w–1-1-onto→z) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
144143r19.23aiv 1789 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (∃y ∈ B [(◡h ‘w) / x]φ → ((w ∈ ω ⋀ ◡h:suc w–1-1-onto→z) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
145144com12 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((w ∈ ω ⋀ ◡h:suc w–1-1-onto→z) → (∃y ∈ B [(◡h ‘w) / x]φ → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
146145, 63sylan2 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∃y ∈ B [(◡h ‘w) / x]φ → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
147146imp 348 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∃y ∈ B [(◡h ‘w) / x]φ) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
148 fvex 3843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (◡h ‘w) ∈ V
149 sbcrexg 2045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((◡h ‘w) ∈ V → ([(◡h ‘w) / x]∃y ∈ B φ ↔ ∃y ∈ B [(◡h ‘w) / x]φ))
150148, 149ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ([(◡h ‘w) / x]∃y ∈ B φ ↔ ∃y ∈ B [(◡h ‘w) / x]φ)
151147, 150sylan2b 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ [(◡h ‘w) / x]∃y ∈ B φ) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
152148ralsn 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∀x ∈ {(◡h ‘w)}∃y ∈ B φ ↔ [(◡h ‘w) / x]∃y ∈ B φ)
153151, 152sylan2b 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ {(◡h ‘w)}∃y ∈ B φ) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
154126, 153syldan 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
155154com12 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
15615519.23aiv 1333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃g(g:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)[g / f]ψ) → (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
15798, 156sylbi 197 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ) → (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
15886, 157syl6 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀x ∈ (◡h “ w)∃y ∈ B φ → ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
159158com3r 35 . . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → (∀x ∈ (◡h “ w)∃y ∈ B φ → ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
16085, 159mpd 26 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((w ∈ ω ⋀ h:z–1-1-onto→suc w) ⋀ ∀x ∈ z ∃y ∈ B φ) → ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))
161160ex 371 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∀x ∈ z ∃y ∈ B φ → ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
162161com3r 35 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)) → ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
16374, 162syl6 22 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃k k:(◡h “ w)–1-1-onto→w → ((∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))) → ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
164163com3r 35 . . . . . . . . . . . . . . . . . . . 20 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∃k k:(◡h “ w)–1-1-onto→w → ((∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
16573, 164mpd 26 . . . . . . . . . . . . . . . . . . 19 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → ((∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
166 imaexg 3508 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (◡h ∈ V → (◡h “ w) ∈ V)
16767, 166ax-mp 7 . . . . . . . . . . . . . . . . . . . 20 ⊢ (◡h “ w) ∈ V
168 f1oeq2 3793 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = (◡h “ w) → (k:t–1-1-onto→w ↔ k:(◡h “ w)–1-1-onto→w))
169168exbidv 1317 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = (◡h “ w) → (∃k k:t–1-1-onto→w ↔ ∃k k:(◡h “ w)–1-1-onto→w))
170 raleq1 1832 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = (◡h “ w) → (∀x ∈ t ∃y ∈ B φ ↔ ∀x ∈ (◡h “ w)∃y ∈ B φ))
171 feq2 3728 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = (◡h “ w) → (f:t–→B ↔ f:(◡h “ w)–→B))
172 raleq1 1832 . . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t = (◡h “ w) → (∀x ∈ t ψ ↔ ∀x ∈ (◡h “ w)ψ))
173171, 172anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (t = (◡h “ w) → ((f:t–→B ⋀ ∀x ∈ t ψ) ↔ (f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)))
174173exbidv 1317 . . . . . . . . . . . . . . . . . . . . . 22 ⊢ (t = (◡h “ w) → (∃f(f:t–→B ⋀ ∀x ∈ t ψ) ↔ ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)))
175170, 174imbi12d 629 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (t = (◡h “ w) → ((∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)) ↔ (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))))
176169, 175imbi12d 629 . . . . . . . . . . . . . . . . . . . 20 ⊢ (t = (◡h “ w) → ((∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) ↔ (∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ)))))
177167, 176cla4v 1914 . . . . . . . . . . . . . . . . . . 19 ⊢ (∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) → (∃k k:(◡h “ w)–1-1-onto→w → (∀x ∈ (◡h “ w)∃y ∈ B φ → ∃f(f:(◡h “ w)–→B ⋀ ∀x ∈ (◡h “ w)ψ))))
178165, 177syl5 21 . . . . . . . . . . . . . . . . . 18 ⊢ ((w ∈ ω ⋀ h:z–1-1-onto→suc w) → (∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
179178ex 371 . . . . . . . . . . . . . . . . 17 ⊢ (w ∈ ω → (h:z–1-1-onto→suc w → (∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
180179com23 32 . . . . . . . . . . . . . . . 16 ⊢ (w ∈ ω → (∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) → (h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
181180imp 348 . . . . . . . . . . . . . . 15 ⊢ ((w ∈ ω ⋀ ∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))) → (h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
18218119.23adv 1251 . . . . . . . . . . . . . 14 ⊢ ((w ∈ ω ⋀ ∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))) → (∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
183 f1oeq1 3792 . . . . . . . . . . . . . . . . 17 ⊢ (h = k → (h:t–1-1-onto→w ↔ k:t–1-1-onto→w))
184183cbvexv 1353 . . . . . . . . . . . . . . . 16 ⊢ (∃h h:t–1-1-onto→w ↔ ∃k k:t–1-1-onto→w)
185184imbi1i 184 . . . . . . . . . . . . . . 15 ⊢ ((∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) ↔ (∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))))
186185albii 1035 . . . . . . . . . . . . . 14 ⊢ (∀t(∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) ↔ ∀t(∃k k:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))))
187182, 186sylan2b 454 . . . . . . . . . . . . 13 ⊢ ((w ∈ ω ⋀ ∀t(∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))) → (∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
18818719.21aiv 1324 . . . . . . . . . . . 12 ⊢ ((w ∈ ω ⋀ ∀t(∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))) → ∀z(∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
189188ex 371 . . . . . . . . . . 11 ⊢ (w ∈ ω → (∀t(∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))) → ∀z(∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
190 f1oeq2 3793 . . . . . . . . . . . . . 14 ⊢ (z = t → (h:z–1-1-onto→w ↔ h:t–1-1-onto→w))
191190exbidv 1317 . . . . . . . . . . . . 13 ⊢ (z = t → (∃h h:z–1-1-onto→w ↔ ∃h h:t–1-1-onto→w))
192 raleq1 1832 . . . . . . . . . . . . . 14 ⊢ (z = t → (∀x ∈ z ∃y ∈ B φ ↔ ∀x ∈ t ∃y ∈ B φ))
193 feq2 3728 . . . . . . . . . . . . . . . 16 ⊢ (z = t → (f:z–→B ↔ f:t–→B))
194 raleq1 1832 . . . . . . . . . . . . . . . 16 ⊢ (z = t → (∀x ∈ z ψ ↔ ∀x ∈ t ψ))
195193, 194anbi12d 631 . . . . . . . . . . . . . . 15 ⊢ (z = t → ((f:z–→B ⋀ ∀x ∈ z ψ) ↔ (f:t–→B ⋀ ∀x ∈ t ψ)))
196195exbidv 1317 . . . . . . . . . . . . . 14 ⊢ (z = t → (∃f(f:z–→B ⋀ ∀x ∈ z ψ) ↔ ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))
197192, 196imbi12d 629 . . . . . . . . . . . . 13 ⊢ (z = t → ((∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)) ↔ (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))))
198191, 197imbi12d 629 . . . . . . . . . . . 12 ⊢ (z = t → ((∃h h:z–1-1-onto→w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ (∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ)))))
199198cbvalv 1352 . . . . . . . . . . 11 ⊢ (∀z(∃h h:z–1-1-onto→w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) ↔ ∀t(∃h h:t–1-1-onto→w → (∀x ∈ t ∃y ∈ B φ → ∃f(f:t–→B ⋀ ∀x ∈ t ψ))))
200189, 199syl5ib 204 . . . . . . . . . 10 ⊢ (w ∈ ω → (∀z(∃h h:z–1-1-onto→w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))) → ∀z(∃h h:z–1-1-onto→suc w → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ)))))
20119, 23, 27, 56, 200finds1 3247 . . . . . . . . 9 ⊢ (m ∈ ω → ∀z(∃h h:z–1-1-onto→m → (∀x ∈ z ∃y ∈ B φ → ∃f(f:z–→B ⋀ ∀x ∈ z ψ))))
20215, 201syl5 21 . . . . . . . 8 ⊢ (A ∈ V → (m ∈ ω → (∃h h:A–1-1-onto→m → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))))
203202com3r 35 . . . . . . 7 ⊢ (∃h h:A–1-1-onto→m → (A ∈ V → (m ∈ ω → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))))
2045, 203sylbi 197 . . . . . 6 ⊢ (A ≈ m → (A ∈ V → (m ∈ ω → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))))
2053, 204mpd 26 . . . . 5 ⊢ (A ≈ m → (m ∈ ω → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ))))
206205com12 11 . . . 4 ⊢ (m ∈ ω → (A ≈ m → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ))))
207206r19.23aiv 1789 . . 3 ⊢ (∃m ∈ ω A ≈ m → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))
2081, 207sylbi 197 . 2 ⊢ (A ∈ Fin → (∀x ∈ A ∃y ∈ B φ → ∃f(f:A–→B ⋀ ∀x ∈ A ψ)))
209208imp 348 1 ⊢ ((A ∈ Fin ⋀ ∀x ∈ A ∃y ∈ B φ) → ∃f(f:A–→B ⋀ ∀x ∈ A ψ))
Colors of variables: wff set class
Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781  ∀wal 990   = wceq 992   ∈ wcel 994  ∃wex 1016  [wsbc 1207  ∀wral 1691  ∃wrex 1692  Vcvv 1857   ∪ cun 2097   ⊆ wss 2099  ∅c0 2332  {csn 2467  <.cop 2469   class class class wbr 2692  suc csuc 2977  ωcom 3218  ◡ccnv 3250  ran crn 3252   ↾ cres 3253   “ cima 3254   Fn wfn 3258  –→wf 3259  –1-1→wf1 3260  –onto→wfo 3261  –1-1-onto→wf1o 3262   ‘cfv 3263   ≈ cen 4505  Fincfn 4508
This theorem is referenced by:  compsub 11488  hscptsscld 11491  alexsublem3 11498  alexsub 11500  comppfsc 11578
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089
This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-sbc 1987  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-en 4509  df-fin 4512
Copyright terms: Public domain