This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fin23lem34

Description: Lemma for fin23 . Establish induction invariants on Y which parameterizes our contradictory chain of subsets. In this section, h is the hypothetically assumed family of subsets, g is the ground set, and i is the induction function constructed in the previous section. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypotheses fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
Assertion fin23lem34 ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 fin23lem.f ⊢ ( 𝜑 → ℎ : ω –1-1→ V )
3 fin23lem.g ⊢ ( 𝜑 → ∪ ran ℎ ⊆ 𝐺 )
4 fin23lem.h ⊢ ( 𝜑 → ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) )
5 fin23lem.i ⊢ 𝑌 = ( rec ( 𝑖 , ℎ ) ↾ ω )
6 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ ∅ ) )
7 f1eq1 ⊢ ( ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ ∅ ) → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ ∅ ) : ω –1-1→ V ) )
8 6 7 syl ⊢ ( 𝑎 = ∅ → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ ∅ ) : ω –1-1→ V ) )
9 6 rneqd ⊢ ( 𝑎 = ∅ → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ ∅ ) )
10 9 unieqd ⊢ ( 𝑎 = ∅ → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ ∅ ) )
11 10 sseq1d ⊢ ( 𝑎 = ∅ → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ) )
12 8 11 anbi12d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ) ) )
13 12 imbi2d ⊢ ( 𝑎 = ∅ → ( ( 𝜑 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ) ↔ ( 𝜑 → ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ) ) ) )
14 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝑏 ) )
15 f1eq1 ⊢ ( ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝑏 ) → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ) )
16 14 15 syl ⊢ ( 𝑎 = 𝑏 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ) )
17 14 rneqd ⊢ ( 𝑎 = 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝑏 ) )
18 17 unieqd ⊢ ( 𝑎 = 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝑏 ) )
19 18 sseq1d ⊢ ( 𝑎 = 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) )
20 16 19 anbi12d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) )
21 20 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ) ↔ ( 𝜑 → ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) ) )
22 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ suc 𝑏 ) )
23 f1eq1 ⊢ ( ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ suc 𝑏 ) → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ) )
24 22 23 syl ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ) )
25 22 rneqd ⊢ ( 𝑎 = suc 𝑏 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ suc 𝑏 ) )
26 25 unieqd ⊢ ( 𝑎 = suc 𝑏 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ suc 𝑏 ) )
27 26 sseq1d ⊢ ( 𝑎 = suc 𝑏 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) )
28 24 27 anbi12d ⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ) )
29 28 imbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝜑 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ) ↔ ( 𝜑 → ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ) ) )
30 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐴 ) )
31 f1eq1 ⊢ ( ( 𝑌 ‘ 𝑎 ) = ( 𝑌 ‘ 𝐴 ) → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ) )
32 30 31 syl ⊢ ( 𝑎 = 𝐴 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ↔ ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ) )
33 30 rneqd ⊢ ( 𝑎 = 𝐴 → ran ( 𝑌 ‘ 𝑎 ) = ran ( 𝑌 ‘ 𝐴 ) )
34 33 unieqd ⊢ ( 𝑎 = 𝐴 → ∪ ran ( 𝑌 ‘ 𝑎 ) = ∪ ran ( 𝑌 ‘ 𝐴 ) )
35 34 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) )
36 32 35 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) ) )
37 36 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝜑 → ( ( 𝑌 ‘ 𝑎 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑎 ) ⊆ 𝐺 ) ) ↔ ( 𝜑 → ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) ) ) )
38 5 fveq1i ⊢ ( 𝑌 ‘ ∅ ) = ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ ∅ )
39 fr0g ⊢ ( ℎ ∈ V → ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ ∅ ) = ℎ )
40 39 elv ⊢ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ ∅ ) = ℎ
41 38 40 eqtri ⊢ ( 𝑌 ‘ ∅ ) = ℎ
42 f1eq1 ⊢ ( ( 𝑌 ‘ ∅ ) = ℎ → ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ↔ ℎ : ω –1-1→ V ) )
43 41 42 ax-mp ⊢ ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ↔ ℎ : ω –1-1→ V )
44 41 rneqi ⊢ ran ( 𝑌 ‘ ∅ ) = ran ℎ
45 44 unieqi ⊢ ∪ ran ( 𝑌 ‘ ∅ ) = ∪ ran ℎ
46 45 sseq1i ⊢ ( ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ↔ ∪ ran ℎ ⊆ 𝐺 )
47 43 46 anbi12i ⊢ ( ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ) ↔ ( ℎ : ω –1-1→ V ∧ ∪ ran ℎ ⊆ 𝐺 ) )
48 2 3 47 sylanbrc ⊢ ( 𝜑 → ( ( 𝑌 ‘ ∅ ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ ∅ ) ⊆ 𝐺 ) )
49 fvex ⊢ ( 𝑌 ‘ 𝑏 ) ∈ V
50 f1eq1 ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( 𝑗 : ω –1-1→ V ↔ ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ) )
51 rneq ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ran 𝑗 = ran ( 𝑌 ‘ 𝑏 ) )
52 51 unieqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ∪ ran 𝑗 = ∪ ran ( 𝑌 ‘ 𝑏 ) )
53 52 sseq1d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ∪ ran 𝑗 ⊆ 𝐺 ↔ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) )
54 50 53 anbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) ↔ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) )
55 fveq2 ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
56 f1eq1 ⊢ ( ( 𝑖 ‘ 𝑗 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ↔ ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ) )
57 55 56 syl ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ↔ ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ) )
58 55 rneqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ran ( 𝑖 ‘ 𝑗 ) = ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
59 58 unieqd ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ∪ ran ( 𝑖 ‘ 𝑗 ) = ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
60 59 52 psseq12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ↔ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
61 57 60 anbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ↔ ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ) )
62 54 61 imbi12d ⊢ ( 𝑗 = ( 𝑌 ‘ 𝑏 ) → ( ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) ↔ ( ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ) ) )
63 49 62 spcv ⊢ ( ∀ 𝑗 ( ( 𝑗 : ω –1-1→ V ∧ ∪ ran 𝑗 ⊆ 𝐺 ) → ( ( 𝑖 ‘ 𝑗 ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ 𝑗 ) ⊊ ∪ ran 𝑗 ) ) → ( ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ) )
64 4 63 syl ⊢ ( 𝜑 → ( ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) ) )
65 64 imp ⊢ ( ( 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) )
66 pssss ⊢ ( ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) → ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) )
67 sstr ⊢ ( ( ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ ∪ ran ( 𝑌 ‘ 𝑏 ) ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 )
68 66 67 sylan ⊢ ( ( ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 )
69 68 expcom ⊢ ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 → ( ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) → ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) )
70 69 anim2d ⊢ ( ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 → ( ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) ) )
71 70 ad2antll ⊢ ( ( 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊊ ∪ ran ( 𝑌 ‘ 𝑏 ) ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) ) )
72 65 71 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) )
73 72 3adant1 ⊢ ( ( 𝑏 ∈ ω ∧ 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) )
74 frsuc ⊢ ( 𝑏 ∈ ω → ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ suc 𝑏 ) = ( 𝑖 ‘ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝑏 ) ) )
75 5 fveq1i ⊢ ( 𝑌 ‘ suc 𝑏 ) = ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ suc 𝑏 )
76 5 fveq1i ⊢ ( 𝑌 ‘ 𝑏 ) = ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝑏 )
77 76 fveq2i ⊢ ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) = ( 𝑖 ‘ ( ( rec ( 𝑖 , ℎ ) ↾ ω ) ‘ 𝑏 ) )
78 74 75 77 3eqtr4g ⊢ ( 𝑏 ∈ ω → ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
79 f1eq1 ⊢ ( ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ↔ ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ) )
80 rneq ⊢ ( ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ran ( 𝑌 ‘ suc 𝑏 ) = ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
81 80 unieqd ⊢ ( ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ∪ ran ( 𝑌 ‘ suc 𝑏 ) = ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) )
82 81 sseq1d ⊢ ( ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ( ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ↔ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) )
83 79 82 anbi12d ⊢ ( ( 𝑌 ‘ suc 𝑏 ) = ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) → ( ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ↔ ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) ) )
84 78 83 syl ⊢ ( 𝑏 ∈ ω → ( ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ↔ ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) ) )
85 84 3ad2ant1 ⊢ ( ( 𝑏 ∈ ω ∧ 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ↔ ( ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) : ω –1-1→ V ∧ ∪ ran ( 𝑖 ‘ ( 𝑌 ‘ 𝑏 ) ) ⊆ 𝐺 ) ) )
86 73 85 mpbird ⊢ ( ( 𝑏 ∈ ω ∧ 𝜑 ∧ ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) )
87 86 3exp ⊢ ( 𝑏 ∈ ω → ( 𝜑 → ( ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) → ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ) ) )
88 87 a2d ⊢ ( 𝑏 ∈ ω → ( ( 𝜑 → ( ( 𝑌 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝑏 ) ⊆ 𝐺 ) ) → ( 𝜑 → ( ( 𝑌 ‘ suc 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ suc 𝑏 ) ⊆ 𝐺 ) ) ) )
89 13 21 29 37 48 88 finds ⊢ ( 𝐴 ∈ ω → ( 𝜑 → ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) ) )
90 89 impcom ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝑌 ‘ 𝐴 ) : ω –1-1→ V ∧ ∪ ran ( 𝑌 ‘ 𝐴 ) ⊆ 𝐺 ) )