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 = OrdIso E B
hsmexlem.g ⊢ G = OrdIso E ⋃ a ∈ A B
Assertion hsmexlem3 ⊢ A ≼ * D ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → dom ⁡ G ∈ har ⁡ 𝒫 D × C

Proof

Step Hyp Ref Expression
1 hsmexlem.f ⊢ F = OrdIso E B
2 hsmexlem.g ⊢ G = OrdIso E ⋃ a ∈ A B
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 ∈ A B ∈ 𝒫 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 ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → A ∈ V
14 simplr ⊢ A ≼ * D ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → C ∈ On
15 simpr ⊢ A ≼ * D ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C
16 1 2 hsmexlem2 ⊢ A ∈ V ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → dom ⁡ G ∈ har ⁡ 𝒫 A × C
17 13 14 15 16 syl3anc ⊢ A ≼ * D ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → dom ⁡ G ∈ har ⁡ 𝒫 A × C
18 9 17 sseldd ⊢ A ≼ * D ∧ C ∈ On ∧ ∀ a ∈ A B ∈ 𝒫 On ∧ dom ⁡ F ∈ C → dom ⁡ G ∈ har ⁡ 𝒫 D × C