elpglem1

		Ref	Expression
	Assertion	elpglem1	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) → ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 → ( 1^st ‘ 𝐴 ) ⊆ 𝑥 )
2	1	adantl	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → ( 1^st ‘ 𝐴 ) ⊆ 𝑥 )
3		simpl	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → 𝑥 ⊆ Pg )
4	2 3	sstrd	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → ( 1^st ‘ 𝐴 ) ⊆ Pg )
5		elpwi	⊢ ( ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 → ( 2^nd ‘ 𝐴 ) ⊆ 𝑥 )
6	5	adantl	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → ( 2^nd ‘ 𝐴 ) ⊆ 𝑥 )
7		simpl	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → 𝑥 ⊆ Pg )
8	6 7	sstrd	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) → ( 2^nd ‘ 𝐴 ) ⊆ Pg )
9	4 8	anim12dan	⊢ ( ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) → ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )
10	9	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) → ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) )

Metamath Proof Explorer