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 𝐹 = OrdIso ( E , 𝐵 )
hsmexlem.g 𝐺 = OrdIso ( E , 𝑎𝐴 𝐵 )
Assertion hsmexlem3 ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 hsmexlem.f 𝐹 = OrdIso ( E , 𝐵 )
2 hsmexlem.g 𝐺 = OrdIso ( E , 𝑎𝐴 𝐵 )
3 wdomref ( 𝐶 ∈ On → 𝐶* 𝐶 )
4 xpwdomg ( ( 𝐴* 𝐷𝐶* 𝐶 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) )
5 3 4 sylan2 ( ( 𝐴* 𝐷𝐶 ∈ On ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) )
6 wdompwdom ( ( 𝐴 × 𝐶 ) ≼* ( 𝐷 × 𝐶 ) → 𝒫 ( 𝐴 × 𝐶 ) ≼ 𝒫 ( 𝐷 × 𝐶 ) )
7 harword ( 𝒫 ( 𝐴 × 𝐶 ) ≼ 𝒫 ( 𝐷 × 𝐶 ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )
8 5 6 7 3syl ( ( 𝐴* 𝐷𝐶 ∈ On ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )
9 8 adantr ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) ⊆ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )
10 relwdom Rel ≼*
11 10 brrelex1i ( 𝐴* 𝐷𝐴 ∈ V )
12 11 adantr ( ( 𝐴* 𝐷𝐶 ∈ On ) → 𝐴 ∈ V )
13 12 adantr ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → 𝐴 ∈ V )
14 simplr ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → 𝐶 ∈ On )
15 simpr ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) )
16 1 2 hsmexlem2 ( ( 𝐴 ∈ V ∧ 𝐶 ∈ On ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) )
17 13 14 15 16 syl3anc ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐴 × 𝐶 ) ) )
18 9 17 sseldd ( ( ( 𝐴* 𝐷𝐶 ∈ On ) ∧ ∀ 𝑎𝐴 ( 𝐵 ∈ 𝒫 On ∧ dom 𝐹𝐶 ) ) → dom 𝐺 ∈ ( har ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )