Metamath Proof Explorer

Theorem hsmexlem4

Description: Lemma for hsmex . The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypotheses hsmexlem4.x ⊢ 𝑋 ∈ V
hsmexlem4.h ⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
hsmexlem4.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
hsmexlem4.s ⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 }
hsmexlem4.o ⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
Assertion hsmexlem4 ( ( 𝑐 ∈ ω ∧ 𝑑 ∈ 𝑆 ) → dom 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) )

Proof

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 syl5eq ⊢ ( 𝑐 = ∅ → 𝑂 = 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 syl5eq ⊢ ( 𝑐 = 𝑒 → 𝑂 = 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 syl5eq ⊢ ( 𝑐 = 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 𝑂 ∈ ( 𝐻 ‘ 𝑐 ) )