Step |
Hyp |
Ref |
Expression |
1 |
|
hsmexlem4.x |
⊢ 𝑋 ∈ V |
2 |
|
hsmexlem4.h |
⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω ) |
3 |
|
hsmexlem4.u |
⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) ) |
4 |
|
hsmexlem4.s |
⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 } |
5 |
|
hsmexlem4.o |
⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) |
6 |
|
fveq2 |
⊢ ( 𝑐 = ∅ → ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) = ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) |
7 |
6
|
imaeq2d |
⊢ ( 𝑐 = ∅ → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) |
8 |
|
oieq2 |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ) |
9 |
7 8
|
syl |
⊢ ( 𝑐 = ∅ → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ) |
10 |
5 9
|
eqtrid |
⊢ ( 𝑐 = ∅ → 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ) |
11 |
10
|
dmeqd |
⊢ ( 𝑐 = ∅ → dom 𝑂 = dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ) |
12 |
|
fveq2 |
⊢ ( 𝑐 = ∅ → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ ∅ ) ) |
13 |
11 12
|
eleq12d |
⊢ ( 𝑐 = ∅ → ( dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( 𝐻 ‘ ∅ ) ) ) |
14 |
13
|
ralbidv |
⊢ ( 𝑐 = ∅ → ( ∀ 𝑑 ∈ 𝑆 dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( 𝐻 ‘ ∅ ) ) ) |
15 |
|
fveq2 |
⊢ ( 𝑐 = 𝑒 → ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) = ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) |
16 |
15
|
imaeq2d |
⊢ ( 𝑐 = 𝑒 → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) |
17 |
|
oieq2 |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ) |
18 |
16 17
|
syl |
⊢ ( 𝑐 = 𝑒 → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ) |
19 |
5 18
|
eqtrid |
⊢ ( 𝑐 = 𝑒 → 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ) |
20 |
19
|
dmeqd |
⊢ ( 𝑐 = 𝑒 → dom 𝑂 = dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ) |
21 |
|
fveq2 |
⊢ ( 𝑐 = 𝑒 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑒 ) ) |
22 |
20 21
|
eleq12d |
⊢ ( 𝑐 = 𝑒 → ( dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) |
23 |
22
|
ralbidv |
⊢ ( 𝑐 = 𝑒 → ( ∀ 𝑑 ∈ 𝑆 dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) |
24 |
|
fveq2 |
⊢ ( 𝑐 = suc 𝑒 → ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) = ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) |
25 |
24
|
imaeq2d |
⊢ ( 𝑐 = suc 𝑒 → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) |
26 |
|
oieq2 |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ) |
27 |
25 26
|
syl |
⊢ ( 𝑐 = suc 𝑒 → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ) |
28 |
5 27
|
eqtrid |
⊢ ( 𝑐 = suc 𝑒 → 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ) |
29 |
28
|
dmeqd |
⊢ ( 𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ) |
30 |
|
fveq2 |
⊢ ( 𝑐 = suc 𝑒 → ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ suc 𝑒 ) ) |
31 |
29 30
|
eleq12d |
⊢ ( 𝑐 = suc 𝑒 → ( dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) ) |
32 |
31
|
ralbidv |
⊢ ( 𝑐 = suc 𝑒 → ( ∀ 𝑑 ∈ 𝑆 dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ↔ ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) ) |
33 |
|
imassrn |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ⊆ ran rank |
34 |
|
rankf |
⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On |
35 |
|
frn |
⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → ran rank ⊆ On ) |
36 |
34 35
|
ax-mp |
⊢ ran rank ⊆ On |
37 |
33 36
|
sstri |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ⊆ On |
38 |
3
|
ituni0 |
⊢ ( 𝑑 ∈ V → ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) = 𝑑 ) |
39 |
38
|
elv |
⊢ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) = 𝑑 |
40 |
39
|
imaeq2i |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) = ( rank “ 𝑑 ) |
41 |
|
ffun |
⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → Fun rank ) |
42 |
34 41
|
ax-mp |
⊢ Fun rank |
43 |
|
vex |
⊢ 𝑑 ∈ V |
44 |
|
wdomimag |
⊢ ( ( Fun rank ∧ 𝑑 ∈ V ) → ( rank “ 𝑑 ) ≼* 𝑑 ) |
45 |
42 43 44
|
mp2an |
⊢ ( rank “ 𝑑 ) ≼* 𝑑 |
46 |
|
sneq |
⊢ ( 𝑎 = 𝑑 → { 𝑎 } = { 𝑑 } ) |
47 |
46
|
fveq2d |
⊢ ( 𝑎 = 𝑑 → ( TC ‘ { 𝑎 } ) = ( TC ‘ { 𝑑 } ) ) |
48 |
47
|
raleqdv |
⊢ ( 𝑎 = 𝑑 → ( ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 ↔ ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 ) ) |
49 |
48 4
|
elrab2 |
⊢ ( 𝑑 ∈ 𝑆 ↔ ( 𝑑 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 ) ) |
50 |
49
|
simprbi |
⊢ ( 𝑑 ∈ 𝑆 → ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 ) |
51 |
|
snex |
⊢ { 𝑑 } ∈ V |
52 |
|
tcid |
⊢ ( { 𝑑 } ∈ V → { 𝑑 } ⊆ ( TC ‘ { 𝑑 } ) ) |
53 |
51 52
|
ax-mp |
⊢ { 𝑑 } ⊆ ( TC ‘ { 𝑑 } ) |
54 |
|
vsnid |
⊢ 𝑑 ∈ { 𝑑 } |
55 |
53 54
|
sselii |
⊢ 𝑑 ∈ ( TC ‘ { 𝑑 } ) |
56 |
|
breq1 |
⊢ ( 𝑏 = 𝑑 → ( 𝑏 ≼ 𝑋 ↔ 𝑑 ≼ 𝑋 ) ) |
57 |
56
|
rspcv |
⊢ ( 𝑑 ∈ ( TC ‘ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋 ) ) |
58 |
55 57
|
ax-mp |
⊢ ( ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 → 𝑑 ≼ 𝑋 ) |
59 |
|
domwdom |
⊢ ( 𝑑 ≼ 𝑋 → 𝑑 ≼* 𝑋 ) |
60 |
50 58 59
|
3syl |
⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ≼* 𝑋 ) |
61 |
|
wdomtr |
⊢ ( ( ( rank “ 𝑑 ) ≼* 𝑑 ∧ 𝑑 ≼* 𝑋 ) → ( rank “ 𝑑 ) ≼* 𝑋 ) |
62 |
45 60 61
|
sylancr |
⊢ ( 𝑑 ∈ 𝑆 → ( rank “ 𝑑 ) ≼* 𝑋 ) |
63 |
40 62
|
eqbrtrid |
⊢ ( 𝑑 ∈ 𝑆 → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ≼* 𝑋 ) |
64 |
|
eqid |
⊢ OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) |
65 |
64
|
hsmexlem1 |
⊢ ( ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ⊆ On ∧ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ≼* 𝑋 ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( har ‘ 𝒫 𝑋 ) ) |
66 |
37 63 65
|
sylancr |
⊢ ( 𝑑 ∈ 𝑆 → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( har ‘ 𝒫 𝑋 ) ) |
67 |
2
|
hsmexlem7 |
⊢ ( 𝐻 ‘ ∅ ) = ( har ‘ 𝒫 𝑋 ) |
68 |
66 67
|
eleqtrrdi |
⊢ ( 𝑑 ∈ 𝑆 → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( 𝐻 ‘ ∅ ) ) |
69 |
68
|
rgen |
⊢ ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ ∅ ) ) ) ∈ ( 𝐻 ‘ ∅ ) |
70 |
|
nfra1 |
⊢ Ⅎ 𝑑 ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) |
71 |
|
nfv |
⊢ Ⅎ 𝑑 𝑒 ∈ ω |
72 |
70 71
|
nfan |
⊢ Ⅎ 𝑑 ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ 𝑒 ∈ ω ) |
73 |
3
|
ituniiun |
⊢ ( 𝑑 ∈ V → ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) = ∪ 𝑓 ∈ 𝑑 ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) |
74 |
73
|
elv |
⊢ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) = ∪ 𝑓 ∈ 𝑑 ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) |
75 |
74
|
imaeq2i |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) = ( rank “ ∪ 𝑓 ∈ 𝑑 ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) |
76 |
|
imaiun |
⊢ ( rank “ ∪ 𝑓 ∈ 𝑑 ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) = ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) |
77 |
75 76
|
eqtri |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) = ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) |
78 |
|
oieq2 |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) = ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) = OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ) |
79 |
77 78
|
ax-mp |
⊢ OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) = OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) |
80 |
79
|
dmeqi |
⊢ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) = dom OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) |
81 |
60
|
ad2antll |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → 𝑑 ≼* 𝑋 ) |
82 |
2
|
hsmexlem9 |
⊢ ( 𝑒 ∈ ω → ( 𝐻 ‘ 𝑒 ) ∈ On ) |
83 |
82
|
ad2antrl |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → ( 𝐻 ‘ 𝑒 ) ∈ On ) |
84 |
|
fveq2 |
⊢ ( 𝑑 = 𝑓 → ( 𝑈 ‘ 𝑑 ) = ( 𝑈 ‘ 𝑓 ) ) |
85 |
84
|
fveq1d |
⊢ ( 𝑑 = 𝑓 → ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) = ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) |
86 |
85
|
imaeq2d |
⊢ ( 𝑑 = 𝑓 → ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) |
87 |
|
oieq2 |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) = ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ) |
88 |
86 87
|
syl |
⊢ ( 𝑑 = 𝑓 → OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ) |
89 |
88
|
dmeqd |
⊢ ( 𝑑 = 𝑓 → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) = dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ) |
90 |
89
|
eleq1d |
⊢ ( 𝑑 = 𝑓 → ( dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ↔ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) |
91 |
|
simpll |
⊢ ( ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑓 ∈ 𝑑 ) → ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) |
92 |
4
|
ssrab3 |
⊢ 𝑆 ⊆ ∪ ( 𝑅1 “ On ) |
93 |
92
|
sseli |
⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ ( 𝑅1 “ On ) ) |
94 |
|
r1elssi |
⊢ ( 𝑑 ∈ ∪ ( 𝑅1 “ On ) → 𝑑 ⊆ ∪ ( 𝑅1 “ On ) ) |
95 |
93 94
|
syl |
⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ⊆ ∪ ( 𝑅1 “ On ) ) |
96 |
95
|
sselda |
⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑 ) → 𝑓 ∈ ∪ ( 𝑅1 “ On ) ) |
97 |
|
snssi |
⊢ ( 𝑓 ∈ 𝑑 → { 𝑓 } ⊆ 𝑑 ) |
98 |
43
|
tcss |
⊢ ( { 𝑓 } ⊆ 𝑑 → ( TC ‘ { 𝑓 } ) ⊆ ( TC ‘ 𝑑 ) ) |
99 |
97 98
|
syl |
⊢ ( 𝑓 ∈ 𝑑 → ( TC ‘ { 𝑓 } ) ⊆ ( TC ‘ 𝑑 ) ) |
100 |
51
|
tcel |
⊢ ( 𝑑 ∈ { 𝑑 } → ( TC ‘ 𝑑 ) ⊆ ( TC ‘ { 𝑑 } ) ) |
101 |
54 100
|
mp1i |
⊢ ( 𝑓 ∈ 𝑑 → ( TC ‘ 𝑑 ) ⊆ ( TC ‘ { 𝑑 } ) ) |
102 |
99 101
|
sstrd |
⊢ ( 𝑓 ∈ 𝑑 → ( TC ‘ { 𝑓 } ) ⊆ ( TC ‘ { 𝑑 } ) ) |
103 |
|
ssralv |
⊢ ( ( TC ‘ { 𝑓 } ) ⊆ ( TC ‘ { 𝑑 } ) → ( ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 → ∀ 𝑏 ∈ ( TC ‘ { 𝑓 } ) 𝑏 ≼ 𝑋 ) ) |
104 |
102 103
|
syl |
⊢ ( 𝑓 ∈ 𝑑 → ( ∀ 𝑏 ∈ ( TC ‘ { 𝑑 } ) 𝑏 ≼ 𝑋 → ∀ 𝑏 ∈ ( TC ‘ { 𝑓 } ) 𝑏 ≼ 𝑋 ) ) |
105 |
50 104
|
mpan9 |
⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑 ) → ∀ 𝑏 ∈ ( TC ‘ { 𝑓 } ) 𝑏 ≼ 𝑋 ) |
106 |
|
sneq |
⊢ ( 𝑎 = 𝑓 → { 𝑎 } = { 𝑓 } ) |
107 |
106
|
fveq2d |
⊢ ( 𝑎 = 𝑓 → ( TC ‘ { 𝑎 } ) = ( TC ‘ { 𝑓 } ) ) |
108 |
107
|
raleqdv |
⊢ ( 𝑎 = 𝑓 → ( ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 ↔ ∀ 𝑏 ∈ ( TC ‘ { 𝑓 } ) 𝑏 ≼ 𝑋 ) ) |
109 |
108 4
|
elrab2 |
⊢ ( 𝑓 ∈ 𝑆 ↔ ( 𝑓 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑏 ∈ ( TC ‘ { 𝑓 } ) 𝑏 ≼ 𝑋 ) ) |
110 |
96 105 109
|
sylanbrc |
⊢ ( ( 𝑑 ∈ 𝑆 ∧ 𝑓 ∈ 𝑑 ) → 𝑓 ∈ 𝑆 ) |
111 |
110
|
adantll |
⊢ ( ( ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ∧ 𝑓 ∈ 𝑑 ) → 𝑓 ∈ 𝑆 ) |
112 |
111
|
adantll |
⊢ ( ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑓 ∈ 𝑑 ) → 𝑓 ∈ 𝑆 ) |
113 |
90 91 112
|
rspcdva |
⊢ ( ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑓 ∈ 𝑑 ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) |
114 |
|
imassrn |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ⊆ ran rank |
115 |
114 36
|
sstri |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ⊆ On |
116 |
|
fvex |
⊢ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ∈ V |
117 |
116
|
funimaex |
⊢ ( Fun rank → ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ V ) |
118 |
42 117
|
ax-mp |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ V |
119 |
118
|
elpw |
⊢ ( ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ 𝒫 On ↔ ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ⊆ On ) |
120 |
115 119
|
mpbir |
⊢ ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ 𝒫 On |
121 |
113 120
|
jctil |
⊢ ( ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) ∧ 𝑓 ∈ 𝑑 ) → ( ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) |
122 |
121
|
ralrimiva |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ 𝑑 ( ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) |
123 |
|
eqid |
⊢ OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) |
124 |
|
eqid |
⊢ OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) = OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) |
125 |
123 124
|
hsmexlem3 |
⊢ ( ( ( 𝑑 ≼* 𝑋 ∧ ( 𝐻 ‘ 𝑒 ) ∈ On ) ∧ ∀ 𝑓 ∈ 𝑑 ( ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ∈ 𝒫 On ∧ dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ) ) → dom OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑒 ) ) ) ) |
126 |
81 83 122 125
|
syl21anc |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → dom OrdIso ( E , ∪ 𝑓 ∈ 𝑑 ( rank “ ( ( 𝑈 ‘ 𝑓 ) ‘ 𝑒 ) ) ) ∈ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑒 ) ) ) ) |
127 |
80 126
|
eqeltrid |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑒 ) ) ) ) |
128 |
2
|
hsmexlem8 |
⊢ ( 𝑒 ∈ ω → ( 𝐻 ‘ suc 𝑒 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑒 ) ) ) ) |
129 |
128
|
ad2antrl |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → ( 𝐻 ‘ suc 𝑒 ) = ( har ‘ 𝒫 ( 𝑋 × ( 𝐻 ‘ 𝑒 ) ) ) ) |
130 |
127 129
|
eleqtrrd |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ ( 𝑒 ∈ ω ∧ 𝑑 ∈ 𝑆 ) ) → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) |
131 |
130
|
expr |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ 𝑒 ∈ ω ) → ( 𝑑 ∈ 𝑆 → dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) ) |
132 |
72 131
|
ralrimi |
⊢ ( ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) ∧ 𝑒 ∈ ω ) → ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) |
133 |
132
|
expcom |
⊢ ( 𝑒 ∈ ω → ( ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑒 ) ) ) ∈ ( 𝐻 ‘ 𝑒 ) → ∀ 𝑑 ∈ 𝑆 dom OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ suc 𝑒 ) ) ) ∈ ( 𝐻 ‘ suc 𝑒 ) ) ) |
134 |
14 23 32 69 133
|
finds1 |
⊢ ( 𝑐 ∈ ω → ∀ 𝑑 ∈ 𝑆 dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ) |
135 |
134
|
r19.21bi |
⊢ ( ( 𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆 ) → dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) ) |