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

Theorem hsmexlem4 9882
 Description: Lemma for hsmex 9885. 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 6659 . . . . . . . . 9 (𝑐 = ∅ → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘∅))
32imaeq2d 5902 . . . . . . . 8 (𝑐 = ∅ → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘∅)))
4 oieq2 9003 . . . . . . . 8 ((rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘∅)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
53, 4syl 17 . . . . . . 7 (𝑐 = ∅ → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
61, 5syl5eq 2806 . . . . . 6 (𝑐 = ∅ → 𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
76dmeqd 5746 . . . . 5 (𝑐 = ∅ → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))))
8 fveq2 6659 . . . . 5 (𝑐 = ∅ → (𝐻𝑐) = (𝐻‘∅))
97, 8eleq12d 2847 . . . 4 (𝑐 = ∅ → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)))
109ralbidv 3127 . . 3 (𝑐 = ∅ → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)))
11 fveq2 6659 . . . . . . . . 9 (𝑐 = 𝑒 → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘𝑒))
1211imaeq2d 5902 . . . . . . . 8 (𝑐 = 𝑒 → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘𝑒)))
13 oieq2 9003 . . . . . . . 8 ((rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
1412, 13syl 17 . . . . . . 7 (𝑐 = 𝑒 → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑐))) = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
151, 14syl5eq 2806 . . . . . 6 (𝑐 = 𝑒𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
1615dmeqd 5746 . . . . 5 (𝑐 = 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))))
17 fveq2 6659 . . . . 5 (𝑐 = 𝑒 → (𝐻𝑐) = (𝐻𝑒))
1816, 17eleq12d 2847 . . . 4 (𝑐 = 𝑒 → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)))
1918ralbidv 3127 . . 3 (𝑐 = 𝑒 → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)))
20 fveq2 6659 . . . . . . . . 9 (𝑐 = suc 𝑒 → ((𝑈𝑑)‘𝑐) = ((𝑈𝑑)‘suc 𝑒))
2120imaeq2d 5902 . . . . . . . 8 (𝑐 = suc 𝑒 → (rank “ ((𝑈𝑑)‘𝑐)) = (rank “ ((𝑈𝑑)‘suc 𝑒)))
22 oieq2 9003 . . . . . . . 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 2806 . . . . . 6 (𝑐 = suc 𝑒𝑂 = OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
2524dmeqd 5746 . . . . 5 (𝑐 = suc 𝑒 → dom 𝑂 = dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))))
26 fveq2 6659 . . . . 5 (𝑐 = suc 𝑒 → (𝐻𝑐) = (𝐻‘suc 𝑒))
2725, 26eleq12d 2847 . . . 4 (𝑐 = suc 𝑒 → (dom 𝑂 ∈ (𝐻𝑐) ↔ dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
2827ralbidv 3127 . . 3 (𝑐 = suc 𝑒 → (∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐) ↔ ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
29 imassrn 5913 . . . . . . 7 (rank “ ((𝑈𝑑)‘∅)) ⊆ ran rank
30 rankf 9249 . . . . . . . 8 rank: (𝑅1 “ On)⟶On
31 frn 6505 . . . . . . . 8 (rank: (𝑅1 “ On)⟶On → ran rank ⊆ On)
3230, 31ax-mp 5 . . . . . . 7 ran rank ⊆ On
3329, 32sstri 3902 . . . . . 6 (rank “ ((𝑈𝑑)‘∅)) ⊆ On
34 hsmexlem4.u . . . . . . . . . 10 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ 𝑦), 𝑥) ↾ ω))
3534ituni0 9871 . . . . . . . . 9 (𝑑 ∈ V → ((𝑈𝑑)‘∅) = 𝑑)
3635elv 3416 . . . . . . . 8 ((𝑈𝑑)‘∅) = 𝑑
3736imaeq2i 5900 . . . . . . 7 (rank “ ((𝑈𝑑)‘∅)) = (rank “ 𝑑)
38 ffun 6502 . . . . . . . . . 10 (rank: (𝑅1 “ On)⟶On → Fun rank)
3930, 38ax-mp 5 . . . . . . . . 9 Fun rank
40 vex 3414 . . . . . . . . 9 𝑑 ∈ V
41 wdomimag 9077 . . . . . . . . 9 ((Fun rank ∧ 𝑑 ∈ V) → (rank “ 𝑑) ≼* 𝑑)
4239, 40, 41mp2an 692 . . . . . . . 8 (rank “ 𝑑) ≼* 𝑑
43 sneq 4533 . . . . . . . . . . . . 13 (𝑎 = 𝑑 → {𝑎} = {𝑑})
4443fveq2d 6663 . . . . . . . . . . . 12 (𝑎 = 𝑑 → (TC‘{𝑎}) = (TC‘{𝑑}))
4544raleqdv 3330 . . . . . . . . . . 11 (𝑎 = 𝑑 → (∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋))
46 hsmexlem4.s . . . . . . . . . . 11 𝑆 = {𝑎 (𝑅1 “ On) ∣ ∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋}
4745, 46elrab2 3606 . . . . . . . . . 10 (𝑑𝑆 ↔ (𝑑 (𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋))
4847simprbi 501 . . . . . . . . 9 (𝑑𝑆 → ∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋)
49 snex 5301 . . . . . . . . . . . 12 {𝑑} ∈ V
50 tcid 9207 . . . . . . . . . . . 12 ({𝑑} ∈ V → {𝑑} ⊆ (TC‘{𝑑}))
5149, 50ax-mp 5 . . . . . . . . . . 11 {𝑑} ⊆ (TC‘{𝑑})
52 vsnid 4560 . . . . . . . . . . 11 𝑑 ∈ {𝑑}
5351, 52sselii 3890 . . . . . . . . . 10 𝑑 ∈ (TC‘{𝑑})
54 breq1 5036 . . . . . . . . . . 11 (𝑏 = 𝑑 → (𝑏𝑋𝑑𝑋))
5554rspcv 3537 . . . . . . . . . 10 (𝑑 ∈ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋𝑑𝑋))
5653, 55ax-mp 5 . . . . . . . . 9 (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋𝑑𝑋)
57 domwdom 9064 . . . . . . . . 9 (𝑑𝑋𝑑* 𝑋)
5848, 56, 573syl 18 . . . . . . . 8 (𝑑𝑆𝑑* 𝑋)
59 wdomtr 9065 . . . . . . . 8 (((rank “ 𝑑) ≼* 𝑑𝑑* 𝑋) → (rank “ 𝑑) ≼* 𝑋)
6042, 58, 59sylancr 591 . . . . . . 7 (𝑑𝑆 → (rank “ 𝑑) ≼* 𝑋)
6137, 60eqbrtrid 5068 . . . . . 6 (𝑑𝑆 → (rank “ ((𝑈𝑑)‘∅)) ≼* 𝑋)
62 eqid 2759 . . . . . . 7 OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) = OrdIso( E , (rank “ ((𝑈𝑑)‘∅)))
6362hsmexlem1 9879 . . . . . 6 (((rank “ ((𝑈𝑑)‘∅)) ⊆ On ∧ (rank “ ((𝑈𝑑)‘∅)) ≼* 𝑋) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
6433, 61, 63sylancr 591 . . . . 5 (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (har‘𝒫 𝑋))
65 hsmexlem4.h . . . . . 6 𝐻 = (rec((𝑧 ∈ V ↦ (har‘𝒫 (𝑋 × 𝑧))), (har‘𝒫 𝑋)) ↾ ω)
6665hsmexlem7 9876 . . . . 5 (𝐻‘∅) = (har‘𝒫 𝑋)
6764, 66eleqtrrdi 2864 . . . 4 (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅))
6867rgen 3081 . . 3 𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘∅))) ∈ (𝐻‘∅)
69 nfra1 3148 . . . . . 6 𝑑𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒)
70 nfv 1916 . . . . . 6 𝑑 𝑒 ∈ ω
7169, 70nfan 1901 . . . . 5 𝑑(∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω)
7234ituniiun 9875 . . . . . . . . . . . . 13 (𝑑 ∈ V → ((𝑈𝑑)‘suc 𝑒) = 𝑓𝑑 ((𝑈𝑓)‘𝑒))
7372elv 3416 . . . . . . . . . . . 12 ((𝑈𝑑)‘suc 𝑒) = 𝑓𝑑 ((𝑈𝑓)‘𝑒)
7473imaeq2i 5900 . . . . . . . . . . 11 (rank “ ((𝑈𝑑)‘suc 𝑒)) = (rank “ 𝑓𝑑 ((𝑈𝑓)‘𝑒))
75 imaiun 6997 . . . . . . . . . . 11 (rank “ 𝑓𝑑 ((𝑈𝑓)‘𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))
7674, 75eqtri 2782 . . . . . . . . . 10 (rank “ ((𝑈𝑑)‘suc 𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))
77 oieq2 9003 . . . . . . . . . 10 ((rank “ ((𝑈𝑑)‘suc 𝑒)) = 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))))
7876, 77ax-mp 5 . . . . . . . . 9 OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
7978dmeqi 5745 . . . . . . . 8 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) = dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
8058ad2antll 729 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → 𝑑* 𝑋)
8165hsmexlem9 9878 . . . . . . . . . 10 (𝑒 ∈ ω → (𝐻𝑒) ∈ On)
8281ad2antrl 728 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → (𝐻𝑒) ∈ On)
83 fveq2 6659 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑓 → (𝑈𝑑) = (𝑈𝑓))
8483fveq1d 6661 . . . . . . . . . . . . . . . 16 (𝑑 = 𝑓 → ((𝑈𝑑)‘𝑒) = ((𝑈𝑓)‘𝑒))
8584imaeq2d 5902 . . . . . . . . . . . . . . 15 (𝑑 = 𝑓 → (rank “ ((𝑈𝑑)‘𝑒)) = (rank “ ((𝑈𝑓)‘𝑒)))
86 oieq2 9003 . . . . . . . . . . . . . . 15 ((rank “ ((𝑈𝑑)‘𝑒)) = (rank “ ((𝑈𝑓)‘𝑒)) → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8785, 86syl 17 . . . . . . . . . . . . . 14 (𝑑 = 𝑓 → OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8887dmeqd 5746 . . . . . . . . . . . . 13 (𝑑 = 𝑓 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) = dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))))
8988eleq1d 2837 . . . . . . . . . . . 12 (𝑑 = 𝑓 → (dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ↔ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
90 simpll 767 . . . . . . . . . . . 12 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒))
9146ssrab3 3987 . . . . . . . . . . . . . . . . . 18 𝑆 (𝑅1 “ On)
9291sseli 3889 . . . . . . . . . . . . . . . . 17 (𝑑𝑆𝑑 (𝑅1 “ On))
93 r1elssi 9260 . . . . . . . . . . . . . . . . 17 (𝑑 (𝑅1 “ On) → 𝑑 (𝑅1 “ On))
9492, 93syl 17 . . . . . . . . . . . . . . . 16 (𝑑𝑆𝑑 (𝑅1 “ On))
9594sselda 3893 . . . . . . . . . . . . . . 15 ((𝑑𝑆𝑓𝑑) → 𝑓 (𝑅1 “ On))
96 snssi 4699 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑑 → {𝑓} ⊆ 𝑑)
9740tcss 9212 . . . . . . . . . . . . . . . . . . 19 ({𝑓} ⊆ 𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
9896, 97syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓𝑑 → (TC‘{𝑓}) ⊆ (TC‘𝑑))
9949tcel 9213 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ {𝑑} → (TC‘𝑑) ⊆ (TC‘{𝑑}))
10052, 99mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝑓𝑑 → (TC‘𝑑) ⊆ (TC‘{𝑑}))
10198, 100sstrd 3903 . . . . . . . . . . . . . . . . 17 (𝑓𝑑 → (TC‘{𝑓}) ⊆ (TC‘{𝑑}))
102 ssralv 3959 . . . . . . . . . . . . . . . . 17 ((TC‘{𝑓}) ⊆ (TC‘{𝑑}) → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (𝑓𝑑 → (∀𝑏 ∈ (TC‘{𝑑})𝑏𝑋 → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
10448, 103mpan9 511 . . . . . . . . . . . . . . 15 ((𝑑𝑆𝑓𝑑) → ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋)
105 sneq 4533 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑓 → {𝑎} = {𝑓})
106105fveq2d 6663 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑓 → (TC‘{𝑎}) = (TC‘{𝑓}))
107106raleqdv 3330 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑓 → (∀𝑏 ∈ (TC‘{𝑎})𝑏𝑋 ↔ ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
108107, 46elrab2 3606 . . . . . . . . . . . . . . 15 (𝑓𝑆 ↔ (𝑓 (𝑅1 “ On) ∧ ∀𝑏 ∈ (TC‘{𝑓})𝑏𝑋))
10995, 104, 108sylanbrc 587 . . . . . . . . . . . . . 14 ((𝑑𝑆𝑓𝑑) → 𝑓𝑆)
110109adantll 714 . . . . . . . . . . . . 13 (((𝑒 ∈ ω ∧ 𝑑𝑆) ∧ 𝑓𝑑) → 𝑓𝑆)
111110adantll 714 . . . . . . . . . . . 12 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → 𝑓𝑆)
11289, 90, 111rspcdva 3544 . . . . . . . . . . 11 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒))
113 imassrn 5913 . . . . . . . . . . . . 13 (rank “ ((𝑈𝑓)‘𝑒)) ⊆ ran rank
114113, 32sstri 3902 . . . . . . . . . . . 12 (rank “ ((𝑈𝑓)‘𝑒)) ⊆ On
115 fvex 6672 . . . . . . . . . . . . . . 15 ((𝑈𝑓)‘𝑒) ∈ V
116115funimaex 6423 . . . . . . . . . . . . . 14 (Fun rank → (rank “ ((𝑈𝑓)‘𝑒)) ∈ V)
11739, 116ax-mp 5 . . . . . . . . . . . . 13 (rank “ ((𝑈𝑓)‘𝑒)) ∈ V
118117elpw 4499 . . . . . . . . . . . 12 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ↔ (rank “ ((𝑈𝑓)‘𝑒)) ⊆ On)
119114, 118mpbir 234 . . . . . . . . . . 11 (rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On
120112, 119jctil 524 . . . . . . . . . 10 (((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) ∧ 𝑓𝑑) → ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
121120ralrimiva 3114 . . . . . . . . 9 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → ∀𝑓𝑑 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒)))
122 eqid 2759 . . . . . . . . . 10 OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) = OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒)))
123 eqid 2759 . . . . . . . . . 10 OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) = OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒)))
124122, 123hsmexlem3 9881 . . . . . . . . 9 (((𝑑* 𝑋 ∧ (𝐻𝑒) ∈ On) ∧ ∀𝑓𝑑 ((rank “ ((𝑈𝑓)‘𝑒)) ∈ 𝒫 On ∧ dom OrdIso( E , (rank “ ((𝑈𝑓)‘𝑒))) ∈ (𝐻𝑒))) → dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12580, 82, 121, 124syl21anc 837 . . . . . . . 8 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , 𝑓𝑑 (rank “ ((𝑈𝑓)‘𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12679, 125eqeltrid 2857 . . . . . . 7 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (har‘𝒫 (𝑋 × (𝐻𝑒))))
12765hsmexlem8 9877 . . . . . . . 8 (𝑒 ∈ ω → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻𝑒))))
128127ad2antrl 728 . . . . . . 7 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → (𝐻‘suc 𝑒) = (har‘𝒫 (𝑋 × (𝐻𝑒))))
129126, 128eleqtrrd 2856 . . . . . 6 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ (𝑒 ∈ ω ∧ 𝑑𝑆)) → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
130129expr 461 . . . . 5 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω) → (𝑑𝑆 → dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
13171, 130ralrimi 3145 . . . 4 ((∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) ∧ 𝑒 ∈ ω) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒))
132131expcom 418 . . 3 (𝑒 ∈ ω → (∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘𝑒))) ∈ (𝐻𝑒) → ∀𝑑𝑆 dom OrdIso( E , (rank “ ((𝑈𝑑)‘suc 𝑒))) ∈ (𝐻‘suc 𝑒)))
13310, 19, 28, 68, 132finds1 7612 . 2 (𝑐 ∈ ω → ∀𝑑𝑆 dom 𝑂 ∈ (𝐻𝑐))
134133r19.21bi 3138 1 ((𝑐 ∈ ω ∧ 𝑑𝑆) → dom 𝑂 ∈ (𝐻𝑐))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  {crab 3075  Vcvv 3410   ⊆ wss 3859  ∅c0 4226  𝒫 cpw 4495  {csn 4523  ∪ cuni 4799  ∪ ciun 4884   class class class wbr 5033   ↦ cmpt 5113   E cep 5435   × cxp 5523  dom cdm 5525  ran crn 5526   ↾ cres 5527   “ cima 5528  Oncon0 6170  suc csuc 6172  Fun wfun 6330  ⟶wf 6332  ‘cfv 6336  ωcom 7580  reccrdg 8056   ≼ cdom 8526  OrdIsocoi 8999  harchar 9046   ≼* cwdom 9054  TCctc 9204  𝑅1cr1 9217  rankcrnk 9218 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-inf2 9130 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-om 7581  df-1st 7694  df-2nd 7695  df-wrecs 7958  df-smo 7994  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-oi 9000  df-har 9047  df-wdom 9055  df-tc 9205  df-r1 9219  df-rank 9220 This theorem is referenced by:  hsmexlem5  9883
 Copyright terms: Public domain W3C validator