Step |
Hyp |
Ref |
Expression |
1 |
|
axdc3lem2.1 |
⊢ 𝐴 ∈ V |
2 |
|
axdc3lem2.2 |
⊢ 𝑆 = { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } |
3 |
|
axdc3lem2.3 |
⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } ) |
4 |
|
id |
⊢ ( 𝑚 = ∅ → 𝑚 = ∅ ) |
5 |
|
fveq2 |
⊢ ( 𝑚 = ∅ → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ ∅ ) ) |
6 |
5
|
dmeqd |
⊢ ( 𝑚 = ∅ → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ ∅ ) ) |
7 |
4 6
|
eleq12d |
⊢ ( 𝑚 = ∅ → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ ∅ ∈ dom ( ℎ ‘ ∅ ) ) ) |
8 |
|
eleq2 |
⊢ ( 𝑚 = ∅ → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ ∅ ) ) |
9 |
5
|
sseq2d |
⊢ ( 𝑚 = ∅ → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) |
10 |
8 9
|
imbi12d |
⊢ ( 𝑚 = ∅ → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) ) |
11 |
7 10
|
anbi12d |
⊢ ( 𝑚 = ∅ → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) ) ) |
12 |
|
id |
⊢ ( 𝑚 = 𝑖 → 𝑚 = 𝑖 ) |
13 |
|
fveq2 |
⊢ ( 𝑚 = 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑖 ) ) |
14 |
13
|
dmeqd |
⊢ ( 𝑚 = 𝑖 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ 𝑖 ) ) |
15 |
12 14
|
eleq12d |
⊢ ( 𝑚 = 𝑖 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ) ) |
16 |
|
elequ2 |
⊢ ( 𝑚 = 𝑖 → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ 𝑖 ) ) |
17 |
13
|
sseq2d |
⊢ ( 𝑚 = 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) |
18 |
16 17
|
imbi12d |
⊢ ( 𝑚 = 𝑖 → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) ) |
19 |
15 18
|
anbi12d |
⊢ ( 𝑚 = 𝑖 → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) ) ) |
20 |
|
id |
⊢ ( 𝑚 = suc 𝑖 → 𝑚 = suc 𝑖 ) |
21 |
|
fveq2 |
⊢ ( 𝑚 = suc 𝑖 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ suc 𝑖 ) ) |
22 |
21
|
dmeqd |
⊢ ( 𝑚 = suc 𝑖 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ suc 𝑖 ) ) |
23 |
20 22
|
eleq12d |
⊢ ( 𝑚 = suc 𝑖 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) ) |
24 |
|
eleq2 |
⊢ ( 𝑚 = suc 𝑖 → ( 𝑗 ∈ 𝑚 ↔ 𝑗 ∈ suc 𝑖 ) ) |
25 |
21
|
sseq2d |
⊢ ( 𝑚 = suc 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) |
26 |
24 25
|
imbi12d |
⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ↔ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
27 |
23 26
|
anbi12d |
⊢ ( 𝑚 = suc 𝑖 → ( ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ↔ ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) ) |
28 |
|
peano1 |
⊢ ∅ ∈ ω |
29 |
|
ffvelrn |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∅ ∈ ω ) → ( ℎ ‘ ∅ ) ∈ 𝑆 ) |
30 |
28 29
|
mpan2 |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ℎ ‘ ∅ ) ∈ 𝑆 ) |
31 |
|
fdm |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → dom 𝑠 = suc 𝑛 ) |
32 |
|
nnord |
⊢ ( 𝑛 ∈ ω → Ord 𝑛 ) |
33 |
|
0elsuc |
⊢ ( Ord 𝑛 → ∅ ∈ suc 𝑛 ) |
34 |
32 33
|
syl |
⊢ ( 𝑛 ∈ ω → ∅ ∈ suc 𝑛 ) |
35 |
|
peano2 |
⊢ ( 𝑛 ∈ ω → suc 𝑛 ∈ ω ) |
36 |
|
eleq2 |
⊢ ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ suc 𝑛 ) ) |
37 |
|
eleq1 |
⊢ ( dom 𝑠 = suc 𝑛 → ( dom 𝑠 ∈ ω ↔ suc 𝑛 ∈ ω ) ) |
38 |
36 37
|
anbi12d |
⊢ ( dom 𝑠 = suc 𝑛 → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω ) ) ) |
39 |
38
|
biimprcd |
⊢ ( ( ∅ ∈ suc 𝑛 ∧ suc 𝑛 ∈ ω ) → ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) ) |
40 |
34 35 39
|
syl2anc |
⊢ ( 𝑛 ∈ ω → ( dom 𝑠 = suc 𝑛 → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) ) |
41 |
31 40
|
syl5com |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( 𝑛 ∈ ω → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) ) |
42 |
41
|
3ad2ant1 |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) ) |
43 |
42
|
impcom |
⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) |
44 |
43
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ) |
45 |
44
|
ss2abi |
⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } |
46 |
2 45
|
eqsstri |
⊢ 𝑆 ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } |
47 |
46
|
sseli |
⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) |
48 |
|
fvex |
⊢ ( ℎ ‘ ∅ ) ∈ V |
49 |
|
dmeq |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → dom 𝑠 = dom ( ℎ ‘ ∅ ) ) |
50 |
49
|
eleq2d |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ ∅ ) ) ) |
51 |
49
|
eleq1d |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ ∅ ) ∈ ω ) ) |
52 |
50 51
|
anbi12d |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) ) ) |
53 |
48 52
|
elab |
⊢ ( ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) ) |
54 |
47 53
|
sylib |
⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ dom ( ℎ ‘ ∅ ) ∈ ω ) ) |
55 |
54
|
simpld |
⊢ ( ( ℎ ‘ ∅ ) ∈ 𝑆 → ∅ ∈ dom ( ℎ ‘ ∅ ) ) |
56 |
30 55
|
syl |
⊢ ( ℎ : ω ⟶ 𝑆 → ∅ ∈ dom ( ℎ ‘ ∅ ) ) |
57 |
|
noel |
⊢ ¬ 𝑗 ∈ ∅ |
58 |
57
|
pm2.21i |
⊢ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) |
59 |
56 58
|
jctir |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) ) |
60 |
59
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∅ ∈ dom ( ℎ ‘ ∅ ) ∧ ( 𝑗 ∈ ∅ → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ ∅ ) ) ) ) |
61 |
|
ffvelrn |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑖 ∈ ω ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 ) |
62 |
61
|
ancoms |
⊢ ( ( 𝑖 ∈ ω ∧ ℎ : ω ⟶ 𝑆 ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 ) |
63 |
62
|
adantrr |
⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ 𝑖 ) ∈ 𝑆 ) |
64 |
|
suceq |
⊢ ( 𝑘 = 𝑖 → suc 𝑘 = suc 𝑖 ) |
65 |
64
|
fveq2d |
⊢ ( 𝑘 = 𝑖 → ( ℎ ‘ suc 𝑘 ) = ( ℎ ‘ suc 𝑖 ) ) |
66 |
|
2fveq3 |
⊢ ( 𝑘 = 𝑖 → ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) = ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) |
67 |
65 66
|
eleq12d |
⊢ ( 𝑘 = 𝑖 → ( ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) ) |
68 |
67
|
rspcva |
⊢ ( ( 𝑖 ∈ ω ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) |
69 |
68
|
adantrl |
⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) |
70 |
46
|
sseli |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ℎ ‘ 𝑖 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) |
71 |
|
fvex |
⊢ ( ℎ ‘ 𝑖 ) ∈ V |
72 |
|
dmeq |
⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → dom 𝑠 = dom ( ℎ ‘ 𝑖 ) ) |
73 |
72
|
eleq2d |
⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ 𝑖 ) ) ) |
74 |
72
|
eleq1d |
⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ 𝑖 ) ∈ ω ) ) |
75 |
73 74
|
anbi12d |
⊢ ( 𝑠 = ( ℎ ‘ 𝑖 ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) ) ) |
76 |
71 75
|
elab |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) ) |
77 |
70 76
|
sylib |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ∅ ∈ dom ( ℎ ‘ 𝑖 ) ∧ dom ( ℎ ‘ 𝑖 ) ∈ ω ) ) |
78 |
77
|
simprd |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → dom ( ℎ ‘ 𝑖 ) ∈ ω ) |
79 |
|
nnord |
⊢ ( dom ( ℎ ‘ 𝑖 ) ∈ ω → Ord dom ( ℎ ‘ 𝑖 ) ) |
80 |
|
ordsucelsuc |
⊢ ( Ord dom ( ℎ ‘ 𝑖 ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) ) |
81 |
78 79 80
|
3syl |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) ) |
82 |
81
|
adantr |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) ) |
83 |
|
dmeq |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → dom 𝑥 = dom ( ℎ ‘ 𝑖 ) ) |
84 |
|
suceq |
⊢ ( dom 𝑥 = dom ( ℎ ‘ 𝑖 ) → suc dom 𝑥 = suc dom ( ℎ ‘ 𝑖 ) ) |
85 |
83 84
|
syl |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → suc dom 𝑥 = suc dom ( ℎ ‘ 𝑖 ) ) |
86 |
85
|
eqeq2d |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( dom 𝑦 = suc dom 𝑥 ↔ dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ) ) |
87 |
83
|
reseq2d |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( 𝑦 ↾ dom 𝑥 ) = ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) ) |
88 |
|
id |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → 𝑥 = ( ℎ ‘ 𝑖 ) ) |
89 |
87 88
|
eqeq12d |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ↔ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) |
90 |
86 89
|
anbi12d |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → ( ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) ↔ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) ) |
91 |
90
|
rabbidv |
⊢ ( 𝑥 = ( ℎ ‘ 𝑖 ) → { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom 𝑥 ∧ ( 𝑦 ↾ dom 𝑥 ) = 𝑥 ) } = { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ) |
92 |
1 2
|
axdc3lem |
⊢ 𝑆 ∈ V |
93 |
92
|
rabex |
⊢ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ∈ V |
94 |
91 3 93
|
fvmpt |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) = { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ) |
95 |
94
|
eleq2d |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ℎ ‘ suc 𝑖 ) ∈ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ) ) |
96 |
|
dmeq |
⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → dom 𝑦 = dom ( ℎ ‘ suc 𝑖 ) ) |
97 |
96
|
eqeq1d |
⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ↔ dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ) ) |
98 |
|
reseq1 |
⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) ) |
99 |
98
|
eqeq1d |
⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ↔ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) |
100 |
97 99
|
anbi12d |
⊢ ( 𝑦 = ( ℎ ‘ suc 𝑖 ) → ( ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ↔ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) ) |
101 |
100
|
elrab |
⊢ ( ( ℎ ‘ suc 𝑖 ) ∈ { 𝑦 ∈ 𝑆 ∣ ( dom 𝑦 = suc dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑦 ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) } ↔ ( ( ℎ ‘ suc 𝑖 ) ∈ 𝑆 ∧ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) ) |
102 |
95 101
|
bitrdi |
⊢ ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 → ( ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ( ℎ ‘ suc 𝑖 ) ∈ 𝑆 ∧ ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) ) ) |
103 |
102
|
simplbda |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ∧ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) ) |
104 |
103
|
simpld |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → dom ( ℎ ‘ suc 𝑖 ) = suc dom ( ℎ ‘ 𝑖 ) ) |
105 |
104
|
eleq2d |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ↔ suc 𝑖 ∈ suc dom ( ℎ ‘ 𝑖 ) ) ) |
106 |
82 105
|
bitr4d |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ↔ suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) ) |
107 |
106
|
biimpd |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) → suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ) ) |
108 |
103
|
simprd |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) ) |
109 |
|
resss |
⊢ ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) ⊆ ( ℎ ‘ suc 𝑖 ) |
110 |
|
sseq1 |
⊢ ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) → ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) ⊆ ( ℎ ‘ suc 𝑖 ) ↔ ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) |
111 |
109 110
|
mpbii |
⊢ ( ( ( ℎ ‘ suc 𝑖 ) ↾ dom ( ℎ ‘ 𝑖 ) ) = ( ℎ ‘ 𝑖 ) → ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) |
112 |
|
elsuci |
⊢ ( 𝑗 ∈ suc 𝑖 → ( 𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖 ) ) |
113 |
|
pm2.27 |
⊢ ( 𝑗 ∈ 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) |
114 |
|
sstr2 |
⊢ ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) |
115 |
113 114
|
syl6 |
⊢ ( 𝑗 ∈ 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
116 |
|
fveq2 |
⊢ ( 𝑗 = 𝑖 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑖 ) ) |
117 |
116
|
sseq1d |
⊢ ( 𝑗 = 𝑖 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ↔ ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) |
118 |
117
|
biimprd |
⊢ ( 𝑗 = 𝑖 → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) |
119 |
118
|
a1d |
⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
120 |
115 119
|
jaoi |
⊢ ( ( 𝑗 ∈ 𝑖 ∨ 𝑗 = 𝑖 ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
121 |
112 120
|
syl |
⊢ ( 𝑗 ∈ suc 𝑖 → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
122 |
121
|
com13 |
⊢ ( ( ℎ ‘ 𝑖 ) ⊆ ( ℎ ‘ suc 𝑖 ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
123 |
108 111 122
|
3syl |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) → ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) |
124 |
107 123
|
anim12d |
⊢ ( ( ( ℎ ‘ 𝑖 ) ∈ 𝑆 ∧ ( ℎ ‘ suc 𝑖 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) ) |
125 |
63 69 124
|
syl2anc |
⊢ ( ( 𝑖 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) ) |
126 |
125
|
ex |
⊢ ( 𝑖 ∈ ω → ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( 𝑖 ∈ dom ( ℎ ‘ 𝑖 ) ∧ ( 𝑗 ∈ 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑖 ) ) ) → ( suc 𝑖 ∈ dom ( ℎ ‘ suc 𝑖 ) ∧ ( 𝑗 ∈ suc 𝑖 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ suc 𝑖 ) ) ) ) ) ) |
127 |
11 19 27 60 126
|
finds2 |
⊢ ( 𝑚 ∈ ω → ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ) ) |
128 |
127
|
imp |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ∧ ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ) |
129 |
128
|
simprd |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) |
130 |
129
|
expcom |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → ( 𝑗 ∈ 𝑚 → ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) ) |
131 |
130
|
ralrimdv |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) ) |
132 |
131
|
ralrimiv |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) |
133 |
|
frn |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ 𝑆 ) |
134 |
|
ffun |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → Fun 𝑠 ) |
135 |
134
|
3ad2ant1 |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → Fun 𝑠 ) |
136 |
135
|
rexlimivw |
⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → Fun 𝑠 ) |
137 |
136
|
ss2abi |
⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ Fun 𝑠 } |
138 |
2 137
|
eqsstri |
⊢ 𝑆 ⊆ { 𝑠 ∣ Fun 𝑠 } |
139 |
133 138
|
sstrdi |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ Fun 𝑠 } ) |
140 |
139
|
sseld |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑢 ∈ ran ℎ → 𝑢 ∈ { 𝑠 ∣ Fun 𝑠 } ) ) |
141 |
|
vex |
⊢ 𝑢 ∈ V |
142 |
|
funeq |
⊢ ( 𝑠 = 𝑢 → ( Fun 𝑠 ↔ Fun 𝑢 ) ) |
143 |
141 142
|
elab |
⊢ ( 𝑢 ∈ { 𝑠 ∣ Fun 𝑠 } ↔ Fun 𝑢 ) |
144 |
140 143
|
syl6ib |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑢 ∈ ran ℎ → Fun 𝑢 ) ) |
145 |
144
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → Fun 𝑢 ) ) |
146 |
|
ffn |
⊢ ( ℎ : ω ⟶ 𝑆 → ℎ Fn ω ) |
147 |
|
fvelrnb |
⊢ ( ℎ Fn ω → ( 𝑣 ∈ ran ℎ ↔ ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 ) ) |
148 |
|
fvelrnb |
⊢ ( ℎ Fn ω → ( 𝑢 ∈ ran ℎ ↔ ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 ) ) |
149 |
|
nnord |
⊢ ( 𝑎 ∈ ω → Ord 𝑎 ) |
150 |
|
nnord |
⊢ ( 𝑏 ∈ ω → Ord 𝑏 ) |
151 |
149 150
|
anim12i |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( Ord 𝑎 ∧ Ord 𝑏 ) ) |
152 |
|
ordtri3or |
⊢ ( ( Ord 𝑎 ∧ Ord 𝑏 ) → ( 𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎 ) ) |
153 |
|
fveq2 |
⊢ ( 𝑚 = 𝑏 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑏 ) ) |
154 |
153
|
sseq2d |
⊢ ( 𝑚 = 𝑏 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) |
155 |
154
|
raleqbi1dv |
⊢ ( 𝑚 = 𝑏 → ( ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) |
156 |
155
|
rspcv |
⊢ ( 𝑏 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) |
157 |
|
fveq2 |
⊢ ( 𝑗 = 𝑎 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑎 ) ) |
158 |
157
|
sseq1d |
⊢ ( 𝑗 = 𝑎 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) ↔ ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) |
159 |
158
|
rspccv |
⊢ ( ∀ 𝑗 ∈ 𝑏 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑏 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) |
160 |
156 159
|
syl6 |
⊢ ( 𝑏 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) ) |
161 |
160
|
adantl |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) ) ) |
162 |
161
|
3imp |
⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑎 ∈ 𝑏 ) → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) |
163 |
162
|
orcd |
⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑎 ∈ 𝑏 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
164 |
163
|
3exp |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑎 ∈ 𝑏 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
165 |
164
|
com3r |
⊢ ( 𝑎 ∈ 𝑏 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
166 |
|
fveq2 |
⊢ ( 𝑎 = 𝑏 → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) ) |
167 |
|
eqimss |
⊢ ( ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) → ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ) |
168 |
167
|
orcd |
⊢ ( ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑏 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
169 |
166 168
|
syl |
⊢ ( 𝑎 = 𝑏 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
170 |
169
|
2a1d |
⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
171 |
|
fveq2 |
⊢ ( 𝑚 = 𝑎 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ 𝑎 ) ) |
172 |
171
|
sseq2d |
⊢ ( 𝑚 = 𝑎 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
173 |
172
|
raleqbi1dv |
⊢ ( 𝑚 = 𝑎 → ( ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ↔ ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
174 |
173
|
rspcv |
⊢ ( 𝑎 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
175 |
|
fveq2 |
⊢ ( 𝑗 = 𝑏 → ( ℎ ‘ 𝑗 ) = ( ℎ ‘ 𝑏 ) ) |
176 |
175
|
sseq1d |
⊢ ( 𝑗 = 𝑏 → ( ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
177 |
176
|
rspccv |
⊢ ( ∀ 𝑗 ∈ 𝑎 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑎 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
178 |
174 177
|
syl6 |
⊢ ( 𝑎 ∈ ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) |
179 |
178
|
adantr |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) |
180 |
179
|
3imp |
⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑏 ∈ 𝑎 ) → ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) |
181 |
180
|
olcd |
⊢ ( ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ∧ 𝑏 ∈ 𝑎 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) |
182 |
181
|
3exp |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑏 ∈ 𝑎 → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
183 |
182
|
com3r |
⊢ ( 𝑏 ∈ 𝑎 → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
184 |
165 170 183
|
3jaoi |
⊢ ( ( 𝑎 ∈ 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 ∈ 𝑎 ) → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
185 |
152 184
|
syl |
⊢ ( ( Ord 𝑎 ∧ Ord 𝑏 ) → ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) ) |
186 |
151 185
|
mpcom |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ) ) |
187 |
|
sseq12 |
⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ↔ 𝑢 ⊆ 𝑣 ) ) |
188 |
|
sseq12 |
⊢ ( ( ( ℎ ‘ 𝑏 ) = 𝑣 ∧ ( ℎ ‘ 𝑎 ) = 𝑢 ) → ( ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ 𝑣 ⊆ 𝑢 ) ) |
189 |
188
|
ancoms |
⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ↔ 𝑣 ⊆ 𝑢 ) ) |
190 |
187 189
|
orbi12d |
⊢ ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) ↔ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
191 |
190
|
biimpcd |
⊢ ( ( ( ℎ ‘ 𝑎 ) ⊆ ( ℎ ‘ 𝑏 ) ∨ ( ℎ ‘ 𝑏 ) ⊆ ( ℎ ‘ 𝑎 ) ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
192 |
186 191
|
syl6 |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) |
193 |
192
|
com23 |
⊢ ( ( 𝑎 ∈ ω ∧ 𝑏 ∈ ω ) → ( ( ( ℎ ‘ 𝑎 ) = 𝑢 ∧ ( ℎ ‘ 𝑏 ) = 𝑣 ) → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) |
194 |
193
|
exp4b |
⊢ ( 𝑎 ∈ ω → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑎 ) = 𝑢 → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) ) |
195 |
194
|
com23 |
⊢ ( 𝑎 ∈ ω → ( ( ℎ ‘ 𝑎 ) = 𝑢 → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) ) |
196 |
195
|
rexlimiv |
⊢ ( ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 → ( 𝑏 ∈ ω → ( ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) |
197 |
196
|
rexlimdv |
⊢ ( ∃ 𝑎 ∈ ω ( ℎ ‘ 𝑎 ) = 𝑢 → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) |
198 |
148 197
|
syl6bi |
⊢ ( ℎ Fn ω → ( 𝑢 ∈ ran ℎ → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) |
199 |
198
|
com23 |
⊢ ( ℎ Fn ω → ( ∃ 𝑏 ∈ ω ( ℎ ‘ 𝑏 ) = 𝑣 → ( 𝑢 ∈ ran ℎ → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) |
200 |
147 199
|
sylbid |
⊢ ( ℎ Fn ω → ( 𝑣 ∈ ran ℎ → ( 𝑢 ∈ ran ℎ → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) |
201 |
200
|
com24 |
⊢ ( ℎ Fn ω → ( ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) → ( 𝑢 ∈ ran ℎ → ( 𝑣 ∈ ran ℎ → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) ) |
202 |
201
|
imp |
⊢ ( ( ℎ Fn ω ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ( 𝑣 ∈ ran ℎ → ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) |
203 |
202
|
ralrimdv |
⊢ ( ( ℎ Fn ω ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
204 |
146 203
|
sylan |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
205 |
145 204
|
jcad |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ( 𝑢 ∈ ran ℎ → ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) ) |
206 |
205
|
ralrimiv |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → ∀ 𝑢 ∈ ran ℎ ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) ) |
207 |
|
fununi |
⊢ ( ∀ 𝑢 ∈ ran ℎ ( Fun 𝑢 ∧ ∀ 𝑣 ∈ ran ℎ ( 𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢 ) ) → Fun ∪ ran ℎ ) |
208 |
206 207
|
syl |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑚 ∈ ω ∀ 𝑗 ∈ 𝑚 ( ℎ ‘ 𝑗 ) ⊆ ( ℎ ‘ 𝑚 ) ) → Fun ∪ ran ℎ ) |
209 |
132 208
|
syldan |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → Fun ∪ ran ℎ ) |
210 |
|
vex |
⊢ 𝑚 ∈ V |
211 |
210
|
eldm2 |
⊢ ( 𝑚 ∈ dom ∪ ran ℎ ↔ ∃ 𝑢 〈 𝑚 , 𝑢 〉 ∈ ∪ ran ℎ ) |
212 |
|
eluni2 |
⊢ ( 〈 𝑚 , 𝑢 〉 ∈ ∪ ran ℎ ↔ ∃ 𝑣 ∈ ran ℎ 〈 𝑚 , 𝑢 〉 ∈ 𝑣 ) |
213 |
210 141
|
opeldm |
⊢ ( 〈 𝑚 , 𝑢 〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣 ) |
214 |
213
|
a1i |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 〈 𝑚 , 𝑢 〉 ∈ 𝑣 → 𝑚 ∈ dom 𝑣 ) ) |
215 |
133 46
|
sstrdi |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) |
216 |
|
ssel |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → ( 𝑣 ∈ ran ℎ → 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) ) |
217 |
|
vex |
⊢ 𝑣 ∈ V |
218 |
|
dmeq |
⊢ ( 𝑠 = 𝑣 → dom 𝑠 = dom 𝑣 ) |
219 |
218
|
eleq2d |
⊢ ( 𝑠 = 𝑣 → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom 𝑣 ) ) |
220 |
218
|
eleq1d |
⊢ ( 𝑠 = 𝑣 → ( dom 𝑠 ∈ ω ↔ dom 𝑣 ∈ ω ) ) |
221 |
219 220
|
anbi12d |
⊢ ( 𝑠 = 𝑣 → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) ) ) |
222 |
217 221
|
elab |
⊢ ( 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) ) |
223 |
222
|
simprbi |
⊢ ( 𝑣 ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → dom 𝑣 ∈ ω ) |
224 |
216 223
|
syl6 |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } → ( 𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω ) ) |
225 |
215 224
|
syl |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑣 ∈ ran ℎ → dom 𝑣 ∈ ω ) ) |
226 |
214 225
|
anim12d |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ( 〈 𝑚 , 𝑢 〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ ) → ( 𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) ) ) |
227 |
|
elnn |
⊢ ( ( 𝑚 ∈ dom 𝑣 ∧ dom 𝑣 ∈ ω ) → 𝑚 ∈ ω ) |
228 |
226 227
|
syl6 |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ( 〈 𝑚 , 𝑢 〉 ∈ 𝑣 ∧ 𝑣 ∈ ran ℎ ) → 𝑚 ∈ ω ) ) |
229 |
228
|
expcomd |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑣 ∈ ran ℎ → ( 〈 𝑚 , 𝑢 〉 ∈ 𝑣 → 𝑚 ∈ ω ) ) ) |
230 |
229
|
rexlimdv |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ∃ 𝑣 ∈ ran ℎ 〈 𝑚 , 𝑢 〉 ∈ 𝑣 → 𝑚 ∈ ω ) ) |
231 |
212 230
|
syl5bi |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 〈 𝑚 , 𝑢 〉 ∈ ∪ ran ℎ → 𝑚 ∈ ω ) ) |
232 |
231
|
exlimdv |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ∃ 𝑢 〈 𝑚 , 𝑢 〉 ∈ ∪ ran ℎ → 𝑚 ∈ ω ) ) |
233 |
211 232
|
syl5bi |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω ) ) |
234 |
233
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ∪ ran ℎ → 𝑚 ∈ ω ) ) |
235 |
|
id |
⊢ ( 𝑚 ∈ ω → 𝑚 ∈ ω ) |
236 |
|
fnfvelrn |
⊢ ( ( ℎ Fn ω ∧ 𝑚 ∈ ω ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ ) |
237 |
146 235 236
|
syl2anr |
⊢ ( ( 𝑚 ∈ ω ∧ ℎ : ω ⟶ 𝑆 ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ ) |
238 |
237
|
adantrr |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → ( ℎ ‘ 𝑚 ) ∈ ran ℎ ) |
239 |
128
|
simpld |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) |
240 |
|
dmeq |
⊢ ( 𝑢 = ( ℎ ‘ 𝑚 ) → dom 𝑢 = dom ( ℎ ‘ 𝑚 ) ) |
241 |
240
|
eliuni |
⊢ ( ( ( ℎ ‘ 𝑚 ) ∈ ran ℎ ∧ 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎ dom 𝑢 ) |
242 |
238 239 241
|
syl2anc |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ ∪ 𝑢 ∈ ran ℎ dom 𝑢 ) |
243 |
|
dmuni |
⊢ dom ∪ ran ℎ = ∪ 𝑢 ∈ ran ℎ dom 𝑢 |
244 |
242 243
|
eleqtrrdi |
⊢ ( ( 𝑚 ∈ ω ∧ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ) → 𝑚 ∈ dom ∪ ran ℎ ) |
245 |
244
|
expcom |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → 𝑚 ∈ dom ∪ ran ℎ ) ) |
246 |
234 245
|
impbid |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ dom ∪ ran ℎ ↔ 𝑚 ∈ ω ) ) |
247 |
246
|
eqrdv |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → dom ∪ ran ℎ = ω ) |
248 |
|
rnuni |
⊢ ran ∪ ran ℎ = ∪ 𝑠 ∈ ran ℎ ran 𝑠 |
249 |
|
frn |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ran 𝑠 ⊆ 𝐴 ) |
250 |
249
|
3ad2ant1 |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ran 𝑠 ⊆ 𝐴 ) |
251 |
250
|
rexlimivw |
⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ran 𝑠 ⊆ 𝐴 ) |
252 |
251
|
ss2abi |
⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } |
253 |
2 252
|
eqsstri |
⊢ 𝑆 ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } |
254 |
133 253
|
sstrdi |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } ) |
255 |
|
ssel |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } → ( 𝑠 ∈ ran ℎ → 𝑠 ∈ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } ) ) |
256 |
|
abid |
⊢ ( 𝑠 ∈ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } ↔ ran 𝑠 ⊆ 𝐴 ) |
257 |
255 256
|
syl6ib |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ran 𝑠 ⊆ 𝐴 } → ( 𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴 ) ) |
258 |
254 257
|
syl |
⊢ ( ℎ : ω ⟶ 𝑆 → ( 𝑠 ∈ ran ℎ → ran 𝑠 ⊆ 𝐴 ) ) |
259 |
258
|
ralrimiv |
⊢ ( ℎ : ω ⟶ 𝑆 → ∀ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 ) |
260 |
|
iunss |
⊢ ( ∪ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 ↔ ∀ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 ) |
261 |
259 260
|
sylibr |
⊢ ( ℎ : ω ⟶ 𝑆 → ∪ 𝑠 ∈ ran ℎ ran 𝑠 ⊆ 𝐴 ) |
262 |
248 261
|
eqsstrid |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ∪ ran ℎ ⊆ 𝐴 ) |
263 |
262
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ran ∪ ran ℎ ⊆ 𝐴 ) |
264 |
|
df-fn |
⊢ ( ∪ ran ℎ Fn ω ↔ ( Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω ) ) |
265 |
|
df-f |
⊢ ( ∪ ran ℎ : ω ⟶ 𝐴 ↔ ( ∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴 ) ) |
266 |
265
|
biimpri |
⊢ ( ( ∪ ran ℎ Fn ω ∧ ran ∪ ran ℎ ⊆ 𝐴 ) → ∪ ran ℎ : ω ⟶ 𝐴 ) |
267 |
264 266
|
sylanbr |
⊢ ( ( ( Fun ∪ ran ℎ ∧ dom ∪ ran ℎ = ω ) ∧ ran ∪ ran ℎ ⊆ 𝐴 ) → ∪ ran ℎ : ω ⟶ 𝐴 ) |
268 |
209 247 263 267
|
syl21anc |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∪ ran ℎ : ω ⟶ 𝐴 ) |
269 |
|
fnfvelrn |
⊢ ( ( ℎ Fn ω ∧ ∅ ∈ ω ) → ( ℎ ‘ ∅ ) ∈ ran ℎ ) |
270 |
146 28 269
|
sylancl |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ℎ ‘ ∅ ) ∈ ran ℎ ) |
271 |
270
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ ∅ ) ∈ ran ℎ ) |
272 |
|
elssuni |
⊢ ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ ) |
273 |
271 272
|
syl |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ ) |
274 |
56
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∅ ∈ dom ( ℎ ‘ ∅ ) ) |
275 |
|
funssfv |
⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ ∅ ) ⊆ ∪ ran ℎ ∧ ∅ ∈ dom ( ℎ ‘ ∅ ) ) → ( ∪ ran ℎ ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) ) |
276 |
209 273 274 275
|
syl3anc |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∪ ran ℎ ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) ) |
277 |
|
simp2 |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑠 ‘ ∅ ) = 𝐶 ) |
278 |
277
|
rexlimivw |
⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑠 ‘ ∅ ) = 𝐶 ) |
279 |
278
|
ss2abi |
⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } |
280 |
2 279
|
eqsstri |
⊢ 𝑆 ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } |
281 |
133 280
|
sstrdi |
⊢ ( ℎ : ω ⟶ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } ) |
282 |
|
ssel |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } ) ) |
283 |
|
fveq1 |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( 𝑠 ‘ ∅ ) = ( ( ℎ ‘ ∅ ) ‘ ∅ ) ) |
284 |
283
|
eqeq1d |
⊢ ( 𝑠 = ( ℎ ‘ ∅ ) → ( ( 𝑠 ‘ ∅ ) = 𝐶 ↔ ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) ) |
285 |
48 284
|
elab |
⊢ ( ( ℎ ‘ ∅ ) ∈ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } ↔ ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) |
286 |
282 285
|
syl6ib |
⊢ ( ran ℎ ⊆ { 𝑠 ∣ ( 𝑠 ‘ ∅ ) = 𝐶 } → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) ) |
287 |
281 286
|
syl |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) ) |
288 |
287
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( ℎ ‘ ∅ ) ∈ ran ℎ → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) ) |
289 |
271 288
|
mpd |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ( ℎ ‘ ∅ ) ‘ ∅ ) = 𝐶 ) |
290 |
276 289
|
eqtrd |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ) |
291 |
|
nfv |
⊢ Ⅎ 𝑘 ℎ : ω ⟶ 𝑆 |
292 |
|
nfra1 |
⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) |
293 |
291 292
|
nfan |
⊢ Ⅎ 𝑘 ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) |
294 |
133
|
ad2antrr |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ran ℎ ⊆ 𝑆 ) |
295 |
|
peano2 |
⊢ ( 𝑘 ∈ ω → suc 𝑘 ∈ ω ) |
296 |
|
fnfvelrn |
⊢ ( ( ℎ Fn ω ∧ suc 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ ) |
297 |
146 295 296
|
syl2an |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ ) |
298 |
297
|
adantlr |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ ) |
299 |
239
|
expcom |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑚 ∈ ω → 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) ) |
300 |
299
|
ralrimiv |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ) |
301 |
|
id |
⊢ ( 𝑚 = suc 𝑘 → 𝑚 = suc 𝑘 ) |
302 |
|
fveq2 |
⊢ ( 𝑚 = suc 𝑘 → ( ℎ ‘ 𝑚 ) = ( ℎ ‘ suc 𝑘 ) ) |
303 |
302
|
dmeqd |
⊢ ( 𝑚 = suc 𝑘 → dom ( ℎ ‘ 𝑚 ) = dom ( ℎ ‘ suc 𝑘 ) ) |
304 |
301 303
|
eleq12d |
⊢ ( 𝑚 = suc 𝑘 → ( 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) ↔ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
305 |
304
|
rspcv |
⊢ ( suc 𝑘 ∈ ω → ( ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
306 |
295 305
|
syl |
⊢ ( 𝑘 ∈ ω → ( ∀ 𝑚 ∈ ω 𝑚 ∈ dom ( ℎ ‘ 𝑚 ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
307 |
300 306
|
mpan9 |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) |
308 |
|
eleq2 |
⊢ ( dom 𝑠 = suc 𝑛 → ( suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ suc 𝑛 ) ) |
309 |
308
|
biimpa |
⊢ ( ( dom 𝑠 = suc 𝑛 ∧ suc 𝑘 ∈ dom 𝑠 ) → suc 𝑘 ∈ suc 𝑛 ) |
310 |
31 309
|
sylan |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ suc 𝑘 ∈ dom 𝑠 ) → suc 𝑘 ∈ suc 𝑛 ) |
311 |
|
ordsucelsuc |
⊢ ( Ord 𝑛 → ( 𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛 ) ) |
312 |
32 311
|
syl |
⊢ ( 𝑛 ∈ ω → ( 𝑘 ∈ 𝑛 ↔ suc 𝑘 ∈ suc 𝑛 ) ) |
313 |
312
|
biimprd |
⊢ ( 𝑛 ∈ ω → ( suc 𝑘 ∈ suc 𝑛 → 𝑘 ∈ 𝑛 ) ) |
314 |
|
rsp |
⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑘 ∈ 𝑛 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) |
315 |
313 314
|
syl9r |
⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ suc 𝑛 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) |
316 |
315
|
com13 |
⊢ ( suc 𝑘 ∈ suc 𝑛 → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) |
317 |
310 316
|
syl |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ suc 𝑘 ∈ dom 𝑠 ) → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) |
318 |
317
|
ex |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑛 ∈ ω → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) ) |
319 |
318
|
com24 |
⊢ ( 𝑠 : suc 𝑛 ⟶ 𝐴 → ( ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) ) |
320 |
319
|
imp |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) |
321 |
320
|
3adant2 |
⊢ ( ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑛 ∈ ω → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) ) |
322 |
321
|
impcom |
⊢ ( ( 𝑛 ∈ ω ∧ ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) |
323 |
322
|
rexlimiva |
⊢ ( ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) → ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ) |
324 |
323
|
ss2abi |
⊢ { 𝑠 ∣ ∃ 𝑛 ∈ ω ( 𝑠 : suc 𝑛 ⟶ 𝐴 ∧ ( 𝑠 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ 𝑛 ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } |
325 |
2 324
|
eqsstri |
⊢ 𝑆 ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } |
326 |
|
sstr |
⊢ ( ( ran ℎ ⊆ 𝑆 ∧ 𝑆 ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) → ran ℎ ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) |
327 |
325 326
|
mpan2 |
⊢ ( ran ℎ ⊆ 𝑆 → ran ℎ ⊆ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) |
328 |
327
|
sseld |
⊢ ( ran ℎ ⊆ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ) ) |
329 |
|
fvex |
⊢ ( ℎ ‘ suc 𝑘 ) ∈ V |
330 |
|
dmeq |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → dom 𝑠 = dom ( ℎ ‘ suc 𝑘 ) ) |
331 |
330
|
eleq2d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( suc 𝑘 ∈ dom 𝑠 ↔ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
332 |
|
fveq1 |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝑠 ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ) |
333 |
|
fveq1 |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝑠 ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) |
334 |
333
|
fveq2d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) |
335 |
332 334
|
eleq12d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) |
336 |
331 335
|
imbi12d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) ↔ ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) ) |
337 |
329 336
|
elab |
⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( suc 𝑘 ∈ dom 𝑠 → ( 𝑠 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑠 ‘ 𝑘 ) ) ) } ↔ ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) |
338 |
328 337
|
syl6ib |
⊢ ( ran ℎ ⊆ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) ) |
339 |
294 298 307 338
|
syl3c |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) |
340 |
209
|
adantr |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → Fun ∪ ran ℎ ) |
341 |
|
elssuni |
⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ) |
342 |
297 341
|
syl |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ) |
343 |
342
|
adantlr |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ) |
344 |
|
funssfv |
⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ∧ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ) |
345 |
340 343 307 344
|
syl3anc |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ) |
346 |
215
|
sseld |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ) ) |
347 |
330
|
eleq2d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ∅ ∈ dom 𝑠 ↔ ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
348 |
330
|
eleq1d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( dom 𝑠 ∈ ω ↔ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) |
349 |
347 348
|
anbi12d |
⊢ ( 𝑠 = ( ℎ ‘ suc 𝑘 ) → ( ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) ↔ ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) ) |
350 |
329 349
|
elab |
⊢ ( ( ℎ ‘ suc 𝑘 ) ∈ { 𝑠 ∣ ( ∅ ∈ dom 𝑠 ∧ dom 𝑠 ∈ ω ) } ↔ ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) |
351 |
346 350
|
syl6ib |
⊢ ( ℎ : ω ⟶ 𝑆 → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) ) |
352 |
351
|
adantr |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ( ℎ ‘ suc 𝑘 ) ∈ ran ℎ → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) ) |
353 |
297 352
|
mpd |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( ∅ ∈ dom ( ℎ ‘ suc 𝑘 ) ∧ dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) ) |
354 |
353
|
simprd |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → dom ( ℎ ‘ suc 𝑘 ) ∈ ω ) |
355 |
|
nnord |
⊢ ( dom ( ℎ ‘ suc 𝑘 ) ∈ ω → Ord dom ( ℎ ‘ suc 𝑘 ) ) |
356 |
|
ordtr |
⊢ ( Ord dom ( ℎ ‘ suc 𝑘 ) → Tr dom ( ℎ ‘ suc 𝑘 ) ) |
357 |
|
trsuc |
⊢ ( ( Tr dom ( ℎ ‘ suc 𝑘 ) ∧ suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) |
358 |
357
|
ex |
⊢ ( Tr dom ( ℎ ‘ suc 𝑘 ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
359 |
354 355 356 358
|
4syl |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ 𝑘 ∈ ω ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
360 |
359
|
adantlr |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( suc 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) ) |
361 |
307 360
|
mpd |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) |
362 |
|
funssfv |
⊢ ( ( Fun ∪ ran ℎ ∧ ( ℎ ‘ suc 𝑘 ) ⊆ ∪ ran ℎ ∧ 𝑘 ∈ dom ( ℎ ‘ suc 𝑘 ) ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) |
363 |
340 343 361 362
|
syl3anc |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) |
364 |
|
simpl |
⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ) |
365 |
|
simpr |
⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) |
366 |
365
|
fveq2d |
⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) |
367 |
364 366
|
eleq12d |
⊢ ( ( ( ∪ ran ℎ ‘ suc 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∧ ( ∪ ran ℎ ‘ 𝑘 ) = ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) → ( ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) |
368 |
345 363 367
|
syl2anc |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ↔ ( ( ℎ ‘ suc 𝑘 ) ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ( ℎ ‘ suc 𝑘 ) ‘ 𝑘 ) ) ) ) |
369 |
339 368
|
mpbird |
⊢ ( ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) ∧ 𝑘 ∈ ω ) → ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) |
370 |
369
|
ex |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ω → ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) ) |
371 |
293 370
|
ralrimi |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) |
372 |
|
vex |
⊢ ℎ ∈ V |
373 |
372
|
rnex |
⊢ ran ℎ ∈ V |
374 |
373
|
uniex |
⊢ ∪ ran ℎ ∈ V |
375 |
|
feq1 |
⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 : ω ⟶ 𝐴 ↔ ∪ ran ℎ : ω ⟶ 𝐴 ) ) |
376 |
|
fveq1 |
⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ ∅ ) = ( ∪ ran ℎ ‘ ∅ ) ) |
377 |
376
|
eqeq1d |
⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 ‘ ∅ ) = 𝐶 ↔ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ) ) |
378 |
|
fveq1 |
⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ suc 𝑘 ) = ( ∪ ran ℎ ‘ suc 𝑘 ) ) |
379 |
|
fveq1 |
⊢ ( 𝑔 = ∪ ran ℎ → ( 𝑔 ‘ 𝑘 ) = ( ∪ ran ℎ ‘ 𝑘 ) ) |
380 |
379
|
fveq2d |
⊢ ( 𝑔 = ∪ ran ℎ → ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) |
381 |
378 380
|
eleq12d |
⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) ) |
382 |
381
|
ralbidv |
⊢ ( 𝑔 = ∪ ran ℎ → ( ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ↔ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) ) |
383 |
375 377 382
|
3anbi123d |
⊢ ( 𝑔 = ∪ ran ℎ → ( ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ↔ ( ∪ ran ℎ : ω ⟶ 𝐴 ∧ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) ) ) |
384 |
374 383
|
spcev |
⊢ ( ( ∪ ran ℎ : ω ⟶ 𝐴 ∧ ( ∪ ran ℎ ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( ∪ ran ℎ ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( ∪ ran ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) |
385 |
268 290 371 384
|
syl3anc |
⊢ ( ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) |
386 |
385
|
exlimiv |
⊢ ( ∃ ℎ ( ℎ : ω ⟶ 𝑆 ∧ ∀ 𝑘 ∈ ω ( ℎ ‘ suc 𝑘 ) ∈ ( 𝐺 ‘ ( ℎ ‘ 𝑘 ) ) ) → ∃ 𝑔 ( 𝑔 : ω ⟶ 𝐴 ∧ ( 𝑔 ‘ ∅ ) = 𝐶 ∧ ∀ 𝑘 ∈ ω ( 𝑔 ‘ suc 𝑘 ) ∈ ( 𝐹 ‘ ( 𝑔 ‘ 𝑘 ) ) ) ) |