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 ‘ 𝒫 ( 𝐷 × 𝐶 ) ) )