Metamath Proof Explorer

Theorem hsmexlem3

Description: Lemma for hsmex . Clear I hypothesis and extend previous result by dominance. Note that this could be substantially strengthened, e.g., using the weak Hartogs function, but all we need here is that there be *some* dominating ordinal. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypotheses hsmexlem.f ⊢F=OrdIsoEB
hsmexlem.g ⊢G=OrdIsoE⋃a∈AB
Assertion hsmexlem3 ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→dom⁡G∈har⁡𝒫D×C

Proof

Step Hyp Ref Expression
1 hsmexlem.f ⊢F=OrdIsoEB
2 hsmexlem.g ⊢G=OrdIsoE⋃a∈AB
3 wdomref ⊢C∈On→C≼*C
4 xpwdomg ⊢A≼*D∧C≼*C→A×C≼*D×C
5 3 4 sylan2 ⊢A≼*D∧C∈On→A×C≼*D×C
6 wdompwdom ⊢A×C≼*D×C→𝒫A×C≼𝒫D×C
7 harword ⊢𝒫A×C≼𝒫D×C→har⁡𝒫A×C⊆har⁡𝒫D×C
8 5 6 7 3syl ⊢A≼*D∧C∈On→har⁡𝒫A×C⊆har⁡𝒫D×C
9 8 adantr ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→har⁡𝒫A×C⊆har⁡𝒫D×C
10 relwdom ⊢Rel⁡≼*
11 10 brrelex1i ⊢A≼*D→A∈V
12 11 adantr ⊢A≼*D∧C∈On→A∈V
13 12 adantr ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→A∈V
14 simplr ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→C∈On
15 simpr ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→∀a∈AB∈𝒫On∧dom⁡F∈C
16 1 2 hsmexlem2 ⊢A∈V∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→dom⁡G∈har⁡𝒫A×C
17 13 14 15 16 syl3anc ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→dom⁡G∈har⁡𝒫A×C
18 9 17 sseldd ⊢A≼*D∧C∈On∧∀a∈AB∈𝒫On∧dom⁡F∈C→dom⁡G∈har⁡𝒫D×C