Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = ∅ → (𝑌‘𝑎) = (𝑌‘∅)) |
2 | | f1eq1 6009 |
. . . . . 6
⊢ ((𝑌‘𝑎) = (𝑌‘∅) → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘∅):ω–1-1→V)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝑎 = ∅ → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘∅):ω–1-1→V)) |
4 | 1 | rneqd 5274 |
. . . . . . 7
⊢ (𝑎 = ∅ → ran (𝑌‘𝑎) = ran (𝑌‘∅)) |
5 | 4 | unieqd 4382 |
. . . . . 6
⊢ (𝑎 = ∅ → ∪ ran (𝑌‘𝑎) = ∪ ran (𝑌‘∅)) |
6 | 5 | sseq1d 3595 |
. . . . 5
⊢ (𝑎 = ∅ → (∪ ran (𝑌‘𝑎) ⊆ 𝐺 ↔ ∪ ran
(𝑌‘∅) ⊆
𝐺)) |
7 | 3, 6 | anbi12d 743 |
. . . 4
⊢ (𝑎 = ∅ → (((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺) ↔ ((𝑌‘∅):ω–1-1→V ∧ ∪ ran (𝑌‘∅) ⊆ 𝐺))) |
8 | 7 | imbi2d 329 |
. . 3
⊢ (𝑎 = ∅ → ((𝜑 → ((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺)) ↔ (𝜑 → ((𝑌‘∅):ω–1-1→V ∧ ∪ ran (𝑌‘∅) ⊆ 𝐺)))) |
9 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝑌‘𝑎) = (𝑌‘𝑏)) |
10 | | f1eq1 6009 |
. . . . . 6
⊢ ((𝑌‘𝑎) = (𝑌‘𝑏) → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘𝑏):ω–1-1→V)) |
11 | 9, 10 | syl 17 |
. . . . 5
⊢ (𝑎 = 𝑏 → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘𝑏):ω–1-1→V)) |
12 | 9 | rneqd 5274 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → ran (𝑌‘𝑎) = ran (𝑌‘𝑏)) |
13 | 12 | unieqd 4382 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ∪ ran
(𝑌‘𝑎) = ∪ ran (𝑌‘𝑏)) |
14 | 13 | sseq1d 3595 |
. . . . 5
⊢ (𝑎 = 𝑏 → (∪ ran
(𝑌‘𝑎) ⊆ 𝐺 ↔ ∪ ran
(𝑌‘𝑏) ⊆ 𝐺)) |
15 | 11, 14 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 𝑏 → (((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺) ↔ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺))) |
16 | 15 | imbi2d 329 |
. . 3
⊢ (𝑎 = 𝑏 → ((𝜑 → ((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺)) ↔ (𝜑 → ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)))) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = suc 𝑏 → (𝑌‘𝑎) = (𝑌‘suc 𝑏)) |
18 | | f1eq1 6009 |
. . . . . 6
⊢ ((𝑌‘𝑎) = (𝑌‘suc 𝑏) → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘suc 𝑏):ω–1-1→V)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝑎 = suc 𝑏 → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘suc 𝑏):ω–1-1→V)) |
20 | 17 | rneqd 5274 |
. . . . . . 7
⊢ (𝑎 = suc 𝑏 → ran (𝑌‘𝑎) = ran (𝑌‘suc 𝑏)) |
21 | 20 | unieqd 4382 |
. . . . . 6
⊢ (𝑎 = suc 𝑏 → ∪ ran
(𝑌‘𝑎) = ∪ ran (𝑌‘suc 𝑏)) |
22 | 21 | sseq1d 3595 |
. . . . 5
⊢ (𝑎 = suc 𝑏 → (∪ ran
(𝑌‘𝑎) ⊆ 𝐺 ↔ ∪ ran
(𝑌‘suc 𝑏) ⊆ 𝐺)) |
23 | 19, 22 | anbi12d 743 |
. . . 4
⊢ (𝑎 = suc 𝑏 → (((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺) ↔ ((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺))) |
24 | 23 | imbi2d 329 |
. . 3
⊢ (𝑎 = suc 𝑏 → ((𝜑 → ((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺)) ↔ (𝜑 → ((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺)))) |
25 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑌‘𝑎) = (𝑌‘𝐴)) |
26 | | f1eq1 6009 |
. . . . . 6
⊢ ((𝑌‘𝑎) = (𝑌‘𝐴) → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘𝐴):ω–1-1→V)) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝑌‘𝑎):ω–1-1→V ↔ (𝑌‘𝐴):ω–1-1→V)) |
28 | 25 | rneqd 5274 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → ran (𝑌‘𝑎) = ran (𝑌‘𝐴)) |
29 | 28 | unieqd 4382 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ∪ ran
(𝑌‘𝑎) = ∪ ran (𝑌‘𝐴)) |
30 | 29 | sseq1d 3595 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∪ ran
(𝑌‘𝑎) ⊆ 𝐺 ↔ ∪ ran
(𝑌‘𝐴) ⊆ 𝐺)) |
31 | 27, 30 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 𝐴 → (((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺) ↔ ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺))) |
32 | 31 | imbi2d 329 |
. . 3
⊢ (𝑎 = 𝐴 → ((𝜑 → ((𝑌‘𝑎):ω–1-1→V ∧ ∪ ran (𝑌‘𝑎) ⊆ 𝐺)) ↔ (𝜑 → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺)))) |
33 | | fin23lem.f |
. . . 4
⊢ (𝜑 → ℎ:ω–1-1→V) |
34 | | fin23lem.g |
. . . 4
⊢ (𝜑 → ∪ ran ℎ
⊆ 𝐺) |
35 | | fin23lem.i |
. . . . . . . 8
⊢ 𝑌 = (rec(𝑖, ℎ) ↾ ω) |
36 | 35 | fveq1i 6104 |
. . . . . . 7
⊢ (𝑌‘∅) = ((rec(𝑖, ℎ) ↾
ω)‘∅) |
37 | | vex 3176 |
. . . . . . . 8
⊢ ℎ ∈ V |
38 | | fr0g 7418 |
. . . . . . . 8
⊢ (ℎ ∈ V → ((rec(𝑖, ℎ) ↾ ω)‘∅) = ℎ) |
39 | 37, 38 | ax-mp 5 |
. . . . . . 7
⊢
((rec(𝑖, ℎ) ↾ ω)‘∅)
= ℎ |
40 | 36, 39 | eqtri 2632 |
. . . . . 6
⊢ (𝑌‘∅) = ℎ |
41 | | f1eq1 6009 |
. . . . . 6
⊢ ((𝑌‘∅) = ℎ → ((𝑌‘∅):ω–1-1→V ↔ ℎ:ω–1-1→V)) |
42 | 40, 41 | ax-mp 5 |
. . . . 5
⊢ ((𝑌‘∅):ω–1-1→V ↔ ℎ:ω–1-1→V) |
43 | 40 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑌‘∅) = ran
ℎ |
44 | 43 | unieqi 4381 |
. . . . . 6
⊢ ∪ ran (𝑌‘∅) = ∪ ran ℎ |
45 | 44 | sseq1i 3592 |
. . . . 5
⊢ (∪ ran (𝑌‘∅) ⊆ 𝐺 ↔ ∪ ran
ℎ ⊆ 𝐺) |
46 | 42, 45 | anbi12i 729 |
. . . 4
⊢ (((𝑌‘∅):ω–1-1→V ∧ ∪ ran (𝑌‘∅) ⊆ 𝐺) ↔ (ℎ:ω–1-1→V ∧ ∪ ran ℎ ⊆ 𝐺)) |
47 | 33, 34, 46 | sylanbrc 695 |
. . 3
⊢ (𝜑 → ((𝑌‘∅):ω–1-1→V ∧ ∪ ran (𝑌‘∅) ⊆ 𝐺)) |
48 | | fin23lem.h |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗))) |
49 | | fvex 6113 |
. . . . . . . . . . 11
⊢ (𝑌‘𝑏) ∈ V |
50 | | f1eq1 6009 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑌‘𝑏) → (𝑗:ω–1-1→V ↔ (𝑌‘𝑏):ω–1-1→V)) |
51 | | rneq 5272 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑌‘𝑏) → ran 𝑗 = ran (𝑌‘𝑏)) |
52 | 51 | unieqd 4382 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑌‘𝑏) → ∪ ran
𝑗 = ∪ ran (𝑌‘𝑏)) |
53 | 52 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑌‘𝑏) → (∪ ran
𝑗 ⊆ 𝐺 ↔ ∪ ran
(𝑌‘𝑏) ⊆ 𝐺)) |
54 | 50, 53 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑌‘𝑏) → ((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) ↔ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺))) |
55 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑌‘𝑏) → (𝑖‘𝑗) = (𝑖‘(𝑌‘𝑏))) |
56 | | f1eq1 6009 |
. . . . . . . . . . . . . 14
⊢ ((𝑖‘𝑗) = (𝑖‘(𝑌‘𝑏)) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝑏)):ω–1-1→V)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑌‘𝑏) → ((𝑖‘𝑗):ω–1-1→V ↔ (𝑖‘(𝑌‘𝑏)):ω–1-1→V)) |
58 | 55 | rneqd 5274 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑌‘𝑏) → ran (𝑖‘𝑗) = ran (𝑖‘(𝑌‘𝑏))) |
59 | 58 | unieqd 4382 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑌‘𝑏) → ∪ ran
(𝑖‘𝑗) = ∪ ran (𝑖‘(𝑌‘𝑏))) |
60 | 59, 52 | psseq12d 3663 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑌‘𝑏) → (∪ ran
(𝑖‘𝑗) ⊊ ∪ ran
𝑗 ↔ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏))) |
61 | 57, 60 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑌‘𝑏) → (((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗) ↔ ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏)))) |
62 | 54, 61 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑌‘𝑏) → (((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗)) ↔ (((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏))))) |
63 | 49, 62 | spcv 3272 |
. . . . . . . . . 10
⊢
(∀𝑗((𝑗:ω–1-1→V ∧ ∪ ran 𝑗 ⊆ 𝐺) → ((𝑖‘𝑗):ω–1-1→V ∧ ∪ ran (𝑖‘𝑗) ⊊ ∪ ran
𝑗)) → (((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏)))) |
64 | 48, 63 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏)))) |
65 | 64 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏))) |
66 | | pssss 3664 |
. . . . . . . . . . . 12
⊢ (∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏) → ∪ ran
(𝑖‘(𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘𝑏)) |
67 | | sstr 3576 |
. . . . . . . . . . . 12
⊢ ((∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ ∪ ran
(𝑌‘𝑏) ∧ ∪ ran
(𝑌‘𝑏) ⊆ 𝐺) → ∪ ran
(𝑖‘(𝑌‘𝑏)) ⊆ 𝐺) |
68 | 66, 67 | sylan 487 |
. . . . . . . . . . 11
⊢ ((∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏) ∧ ∪ ran
(𝑌‘𝑏) ⊆ 𝐺) → ∪ ran
(𝑖‘(𝑌‘𝑏)) ⊆ 𝐺) |
69 | 68 | expcom 450 |
. . . . . . . . . 10
⊢ (∪ ran (𝑌‘𝑏) ⊆ 𝐺 → (∪ ran
(𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏) → ∪ ran
(𝑖‘(𝑌‘𝑏)) ⊆ 𝐺)) |
70 | 69 | anim2d 587 |
. . . . . . . . 9
⊢ (∪ ran (𝑌‘𝑏) ⊆ 𝐺 → (((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏)) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺))) |
71 | 70 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → (((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊊ ∪ ran
(𝑌‘𝑏)) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺))) |
72 | 65, 71 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺)) |
73 | 72 | 3adant1 1072 |
. . . . . 6
⊢ ((𝑏 ∈ ω ∧ 𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺)) |
74 | | frsuc 7419 |
. . . . . . . . 9
⊢ (𝑏 ∈ ω →
((rec(𝑖, ℎ) ↾ ω)‘suc 𝑏) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝑏))) |
75 | 35 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝑌‘suc 𝑏) = ((rec(𝑖, ℎ) ↾ ω)‘suc 𝑏) |
76 | 35 | fveq1i 6104 |
. . . . . . . . . 10
⊢ (𝑌‘𝑏) = ((rec(𝑖, ℎ) ↾ ω)‘𝑏) |
77 | 76 | fveq2i 6106 |
. . . . . . . . 9
⊢ (𝑖‘(𝑌‘𝑏)) = (𝑖‘((rec(𝑖, ℎ) ↾ ω)‘𝑏)) |
78 | 74, 75, 77 | 3eqtr4g 2669 |
. . . . . . . 8
⊢ (𝑏 ∈ ω → (𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏))) |
79 | | f1eq1 6009 |
. . . . . . . . 9
⊢ ((𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏)) → ((𝑌‘suc 𝑏):ω–1-1→V ↔ (𝑖‘(𝑌‘𝑏)):ω–1-1→V)) |
80 | | rneq 5272 |
. . . . . . . . . . 11
⊢ ((𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏)) → ran (𝑌‘suc 𝑏) = ran (𝑖‘(𝑌‘𝑏))) |
81 | 80 | unieqd 4382 |
. . . . . . . . . 10
⊢ ((𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏)) → ∪ ran
(𝑌‘suc 𝑏) = ∪
ran (𝑖‘(𝑌‘𝑏))) |
82 | 81 | sseq1d 3595 |
. . . . . . . . 9
⊢ ((𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏)) → (∪ ran
(𝑌‘suc 𝑏) ⊆ 𝐺 ↔ ∪ ran
(𝑖‘(𝑌‘𝑏)) ⊆ 𝐺)) |
83 | 79, 82 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑌‘suc 𝑏) = (𝑖‘(𝑌‘𝑏)) → (((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺) ↔ ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺))) |
84 | 78, 83 | syl 17 |
. . . . . . 7
⊢ (𝑏 ∈ ω → (((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺) ↔ ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺))) |
85 | 84 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝑏 ∈ ω ∧ 𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → (((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺) ↔ ((𝑖‘(𝑌‘𝑏)):ω–1-1→V ∧ ∪ ran (𝑖‘(𝑌‘𝑏)) ⊆ 𝐺))) |
86 | 73, 85 | mpbird 246 |
. . . . 5
⊢ ((𝑏 ∈ ω ∧ 𝜑 ∧ ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → ((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺)) |
87 | 86 | 3exp 1256 |
. . . 4
⊢ (𝑏 ∈ ω → (𝜑 → (((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺) → ((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺)))) |
88 | 87 | a2d 29 |
. . 3
⊢ (𝑏 ∈ ω → ((𝜑 → ((𝑌‘𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘𝑏) ⊆ 𝐺)) → (𝜑 → ((𝑌‘suc 𝑏):ω–1-1→V ∧ ∪ ran (𝑌‘suc 𝑏) ⊆ 𝐺)))) |
89 | 8, 16, 24, 32, 47, 88 | finds 6984 |
. 2
⊢ (𝐴 ∈ ω → (𝜑 → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺))) |
90 | 89 | impcom 445 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑌‘𝐴):ω–1-1→V ∧ ∪ ran (𝑌‘𝐴) ⊆ 𝐺)) |