MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hsmexlem4 Structured version   Visualization version   GIF version

Theorem hsmexlem4 9845
Description: Lemma for hsmex 9848. The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015.)
Hypotheses
Ref Expression
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
Ref Expression
hsmexlem4 ((𝑐 ∈ ω ∧ 𝑑𝑆) → dom 𝑂 ∈ (𝐻𝑐))
Distinct variable groups:   𝑎,𝑐,𝑑,𝐻   𝑆,𝑐,𝑑   𝑈,𝑐,𝑑   𝑎,𝑏,𝑧,𝑋   𝑥,𝑎,𝑦   𝑏,𝑐,𝑑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑧,𝑎,𝑏)   𝑈(𝑥,𝑦,𝑧,𝑎,𝑏)   𝐻(𝑥,𝑦,𝑧,𝑏)   𝑂(𝑥,𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝑋(𝑥,𝑦,𝑐,𝑑)

Proof of Theorem hsmexlem4
Dummy variables 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hsmexlem4.o . . . . . . 7 𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐)))
2 fveq2 6669 . . . . . . . . 9 (𝑐 = ∅ → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘∅))
32imaeq2d 5928 . . . . . . . 8 (𝑐 = ∅ → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘∅)))
4 oieq2 8971 . . . . . . . 8 ((rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘∅)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
53, 4syl 17 . . . . . . 7 (𝑐 = ∅ → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
61, 5syl5eq 2873 . . . . . 6 (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
76dmeqd 5773 . . . . 5 (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
8 fveq2 6669 . . . . 5 (𝑐 = ∅ → (𝐻𝑐) = (𝐻‘∅))
97, 8eleq12d 2912 . . . 4 (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)))
109ralbidv 3202 . . 3 (𝑐 = ∅ → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)))
11 fveq2 6669 . . . . . . . . 9 (𝑐 = 𝑒 → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘𝑒))
1211imaeq2d 5928 . . . . . . . 8 (𝑐 = 𝑒 → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘𝑒)))
13 oieq2 8971 . . . . . . . 8 ((rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
1412, 13syl 17 . . . . . . 7 (𝑐 = 𝑒 → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
151, 14syl5eq 2873 . . . . . 6 (𝑐 = 𝑒𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
1615dmeqd 5773 . . . . 5 (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
17 fveq2 6669 . . . . 5 (𝑐 = 𝑒 → (𝐻𝑐) = (𝐻𝑒))
1816, 17eleq12d 2912 . . . 4 (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)))
1918ralbidv 3202 . . 3 (𝑐 = 𝑒 → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)))
20 fveq2 6669 . . . . . . . . 9 (𝑐 = suc 𝑒 → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘suc 𝑒))
2120imaeq2d 5928 . . . . . . . 8 (𝑐 = suc 𝑒 → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘suc 𝑒)))
22 oieq2 8971 . . . . . . . 8 ((rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘suc 𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
2321, 22syl 17 . . . . . . 7 (𝑐 = suc 𝑒 → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
241, 23syl5eq 2873 . . . . . 6 (𝑐 = suc 𝑒𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
2524dmeqd 5773 . . . . 5 (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
26 fveq2 6669 . . . . 5 (𝑐 = suc 𝑒 → (𝐻𝑐) = (𝐻‘suc 𝑒))
2725, 26eleq12d 2912 . . . 4 (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
2827ralbidv 3202 . . 3 (𝑐 = suc 𝑒 → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29 imassrn 5939 . . . . . . 7 (rank “ ((𝑈𝑑)‘∅)) ⊆ ran rank
30 rankf 9217 . . . . . . . 8 rank: (𝑅1 “ On)⟶On
31 frn 6519 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → ran rank ⊆ On)
3230, 31ax-mp 5 . . . . . . 7 ran rank ⊆ On
3329, 32sstri 3980 . . . . . 6 (rank “ ((𝑈𝑑)‘∅)) ⊆ On
34 hsmexlem4.u . . . . . . . . . 10 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ 𝑦), 𝑥) ↾ ω))
3534ituni0 9834 . . . . . . . . 9 (𝑑 ∈ V → ((𝑈𝑑)‘∅) = 𝑑)
3635elv 3505 . . . . . . . 8 ((𝑈𝑑)‘∅) = 𝑑
3736imaeq2i 5926 . . . . . . 7 (rank “ ((𝑈𝑑)‘∅)) = (rank “ 𝑑)
38 ffun 6516 . . . . . . . . . 10 (rank: (𝑅1 “ On)⟶On → Fun rank)
3930, 38ax-mp 5 . . . . . . . . 9 Fun rank
40 vex 3503 . . . . . . . . 9 𝑑 ∈ V
41 wdomimag 9045 . . . . . . . . 9 ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼* 𝑑)
4239, 40, 41mp2an 688 . . . . . . . 8 (rank “ 𝑑) ≼* 𝑑
43 sneq 4574 . . . . . . . . . . . . 13 (𝑎 = 𝑑 → {𝑎} = {𝑑})
4443fveq2d 6673 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
4544raleqdv 3421 . . . . . . . . . . 11 (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋))
46 hsmexlem4.s . . . . . . . . . . 11 𝑆 = {𝑎 (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋}
4745, 46elrab2 3687 . . . . . . . . . 10 (𝑑𝑆 ↔ (𝑑 (𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋))
4847simprbi 497 . . . . . . . . 9 (𝑑𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋)
49 snex 5328 . . . . . . . . . . . 12 {𝑑} ∈ V
50 tcid 9175 . . . . . . . . . . . 12 ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
5149, 50ax-mp 5 . . . . . . . . . . 11 {𝑑} ⊆ (TC‘{𝑑})
52 vsnid 4599 . . . . . . . . . . 11 𝑑 ∈ {𝑑}
5351, 52sselii 3968 . . . . . . . . . 10 𝑑 ∈ (TC‘{𝑑})
54 breq1 5066 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝑏𝑋𝑑𝑋))
5554rspcv 3622 . . . . . . . . . 10 (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋𝑑𝑋))
5653, 55ax-mp 5 . . . . . . . . 9 (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋𝑑𝑋)
57 domwdom 9032 . . . . . . . . 9 (𝑑𝑋𝑑* 𝑋)
5848, 56, 573syl 18 . . . . . . . 8 (𝑑𝑆𝑑* 𝑋)
59 wdomtr 9033 . . . . . . . 8 (((rank “ 𝑑) ≼* 𝑑𝑑* 𝑋) → (rank “ 𝑑) ≼* 𝑋)
6042, 58, 59sylancr 587 . . . . . . 7 (𝑑𝑆 → (rank “ 𝑑) ≼* 𝑋)
6137, 60eqbrtrid 5098 . . . . . 6 (𝑑𝑆 → (rank “ ((𝑈𝑑)‘∅)) ≼* 𝑋)
62 eqid 2826 . . . . . . 7 OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅)))
6362hsmexlem1 9842 . . . . . 6 (((rank “ ((𝑈𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈𝑑)‘∅)) ≼* 𝑋) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
6433, 61, 63sylancr 587 . . . . 5 (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65 hsmexlem4.h . . . . . 6 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
6665hsmexlem7 9839 . . . . 5 (𝐻‘∅) = (har‘𝒫 𝑋)
6764, 66syl6eleqr 2929 . . . 4 (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅))
6867rgen 3153 . . 3 𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)
69 nfra1 3224 . . . . . 6 𝑑𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)
70 nfv 1908 . . . . . 6 𝑑 𝑒 ∈ ω
7169, 70nfan 1893 . . . . 5 𝑑(∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω)
7234ituniiun 9838 . . . . . . . . . . . . 13 (𝑑 ∈ V → ((𝑈𝑑)‘suc 𝑒) = 𝑓𝑑 ((𝑈𝑓)‘𝑒))
7372elv 3505 . . . . . . . . . . . 12 ((𝑈𝑑)‘suc 𝑒) = 𝑓𝑑 ((𝑈𝑓)‘𝑒)
7473imaeq2i 5926 . . . . . . . . . . 11 (rank “ ((𝑈𝑑)‘suc 𝑒)) = (rank “ 𝑓𝑑 ((𝑈𝑓)‘𝑒))
75 imaiun 7000 . . . . . . . . . . 11 (rank “ 𝑓𝑑 ((𝑈𝑓)‘𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))
7674, 75eqtri 2849 . . . . . . . . . 10 (rank “ ((𝑈𝑑)‘suc 𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))
77 oieq2 8971 . . . . . . . . . 10 ((rank “ ((𝑈𝑑)‘suc 𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))))
7876, 77ax-mp 5 . . . . . . . . 9 OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
7978dmeqi 5772 . . . . . . . 8 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
8058ad2antll 725 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → 𝑑* 𝑋)
8165hsmexlem9 9841 . . . . . . . . . 10 (𝑒 ∈ ω → (𝐻𝑒) ∈ On)
8281ad2antrl 724 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → (𝐻𝑒) ∈ On)
83 fveq2 6669 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑓 → (𝑈𝑑) = (𝑈𝑓))
8483fveq1d 6671 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑓 → ((𝑈𝑑)‘𝑒) = ((𝑈𝑓)‘𝑒))
8584imaeq2d 5928 . . . . . . . . . . . . . . 15 (𝑑 = 𝑓 → (rank “ ((𝑈𝑑)‘𝑒)) = (rank “ ((𝑈𝑓)‘𝑒)))
86 oieq2 8971 . . . . . . . . . . . . . . 15 ((rank “ ((𝑈𝑑)‘𝑒)) = (rank “ ((𝑈𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8785, 86syl 17 . . . . . . . . . . . . . 14 (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8887dmeqd 5773 . . . . . . . . . . . . 13 (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8988eleq1d 2902 . . . . . . . . . . . 12 (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
90 simpll 763 . . . . . . . . . . . 12 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒))
9146ssrab3 4061 . . . . . . . . . . . . . . . . . 18 𝑆 (𝑅1 “ On)
9291sseli 3967 . . . . . . . . . . . . . . . . 17 (𝑑𝑆𝑑 (𝑅1 “ On))
93 r1elssi 9228 . . . . . . . . . . . . . . . . 17 (𝑑 (𝑅1 “ On) → 𝑑 (𝑅1 “ On))
9492, 93syl 17 . . . . . . . . . . . . . . . 16 (𝑑𝑆𝑑 (𝑅1 “ On))
9594sselda 3971 . . . . . . . . . . . . . . 15 ((𝑑𝑆𝑓𝑑) → 𝑓 (𝑅1 “ On))
96 snssi 4740 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑑 → {𝑓} ⊆ 𝑑)
9740tcss 9180 . . . . . . . . . . . . . . . . . . 19 ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
9896, 97syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
9949tcel 9181 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
10052, 99mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝑓𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
10198, 100sstrd 3981 . . . . . . . . . . . . . . . . 17 (𝑓𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102 ssralv 4037 . . . . . . . . . . . . . . . . 17 ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (𝑓𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
10448, 103mpan9 507 . . . . . . . . . . . . . . 15 ((𝑑𝑆𝑓𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋)
105 sneq 4574 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑓 → {𝑎} = {𝑓})
106105fveq2d 6673 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107106raleqdv 3421 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
108107, 46elrab2 3687 . . . . . . . . . . . . . . 15 (𝑓𝑆 ↔ (𝑓 (𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
10995, 104, 108sylanbrc 583 . . . . . . . . . . . . . 14 ((𝑑𝑆𝑓𝑑) → 𝑓𝑆)
110109adantll 710 . . . . . . . . . . . . 13 (((𝑒 ∈ ω ∧ 𝑑𝑆) ∧ 𝑓𝑑) → 𝑓𝑆)
111110adantll 710 . . . . . . . . . . . 12 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → 𝑓𝑆)
11289, 90, 111rspcdva 3629 . . . . . . . . . . 11 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒))
113 imassrn 5939 . . . . . . . . . . . . 13 (rank “ ((𝑈𝑓)‘𝑒)) ⊆ ran rank
114113, 32sstri 3980 . . . . . . . . . . . 12 (rank “ ((𝑈𝑓)‘𝑒)) ⊆ On
115 fvex 6682 . . . . . . . . . . . . . . 15 ((𝑈𝑓)‘𝑒) ∈ V
116115funimaex 6440 . . . . . . . . . . . . . 14 (Fun rank → (rank “ ((𝑈𝑓)‘𝑒)) ∈ V)
11739, 116ax-mp 5 . . . . . . . . . . . . 13 (rank “ ((𝑈𝑓)‘𝑒)) ∈ V
118117elpw 4549 . . . . . . . . . . . 12 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “ ((𝑈𝑓)‘𝑒)) ⊆ On)
119114, 118mpbir 232 . . . . . . . . . . 11 (rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On
120112, 119jctil 520 . . . . . . . . . 10 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
121120ralrimiva 3187 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → ∀𝑓𝑑 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
122 eqid 2826 . . . . . . . . . 10 OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒)))
123 eqid 2826 . . . . . . . . . 10 OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
124122, 123hsmexlem3 9844 . . . . . . . . 9 (((𝑑* 𝑋 ∧ (𝐻𝑒) ∈ On) ∧ ∀𝑓𝑑 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒))) → dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12580, 82, 121, 124syl21anc 835 . . . . . . . 8 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12679, 125eqeltrid 2922 . . . . . . 7 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12765hsmexlem8 9840 . . . . . . . 8 (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻𝑒))))
128127ad2antrl 724 . . . . . . 7 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻𝑒))))
129126, 128eleqtrrd 2921 . . . . . 6 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
130129expr 457 . . . . 5 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω) → (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
13171, 130ralrimi 3221 . . . 4 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
132131expcom 414 . . 3 (𝑒 ∈ ω → (∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
13310, 19, 28, 68, 132finds1 7604 . 2 (𝑐 ∈ ω → ∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐))
134133r19.21bi 3213 1 ((𝑐 ∈ ω ∧ 𝑑𝑆) → dom 𝑂 ∈ (𝐻𝑐))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  wral 3143  {crab 3147  Vcvv 3500  wss 3940  c0 4295  𝒫 cpw 4542  {csn 4564   cuni 4837   ciun 4917   class class class wbr 5063  cmpt 5143   E cep 5463   × cxp 5552  dom cdm 5554  ran crn 5555  cres 5556  cima 5557  Oncon0 6190  suc csuc 6192  Fun wfun 6348  wf 6350  cfv 6354  ωcom 7573  reccrdg 8041  cdom 8501  OrdIsocoi 8967  harchar 9014  * cwdom 9015  TCctc 9172  𝑅1cr1 9185  rankcrnk 9186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-inf2 9098
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-smo 7979  df-recs 8004  df-rdg 8042  df-er 8284  df-en 8504  df-dom 8505  df-sdom 8506  df-oi 8968  df-har 9016  df-wdom 9017  df-tc 9173  df-r1 9187  df-rank 9188
This theorem is referenced by:  hsmexlem5  9846
  Copyright terms: Public domain W3C validator