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 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 𝑂 ∈ ( 𝐻𝑐 ) )