elpglem2

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

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
2		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
3	1 2	unex	⊢ ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) ∈ V
4	3	isseti	⊢ ∃ 𝑥 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) )
5		sseq1	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 𝑥 ⊆ Pg ↔ ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) ⊆ Pg ) )
6		unss	⊢ ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) ↔ ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) ⊆ Pg )
7	5 6	bitr4di	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 𝑥 ⊆ Pg ↔ ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) ) )
8	7	biimprd	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) → 𝑥 ⊆ Pg ) )
9		ssun1	⊢ ( 1^st ‘ 𝐴 ) ⊆ ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) )
10		id	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) )
11	9 10	sseqtrrid	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 1^st ‘ 𝐴 ) ⊆ 𝑥 )
12		vex	⊢ 𝑥 ∈ V
13	12	elpw2	⊢ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ↔ ( 1^st ‘ 𝐴 ) ⊆ 𝑥 )
14	11 13	sylibr	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 )
15		ssun2	⊢ ( 2^nd ‘ 𝐴 ) ⊆ ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) )
16	15 10	sseqtrrid	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 2^nd ‘ 𝐴 ) ⊆ 𝑥 )
17	12	elpw2	⊢ ( ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ↔ ( 2^nd ‘ 𝐴 ) ⊆ 𝑥 )
18	16 17	sylibr	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 )
19	14 18	jca	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) )
20	8 19	jctird	⊢ ( 𝑥 = ( ( 1^st ‘ 𝐴 ) ∪ ( 2^nd ‘ 𝐴 ) ) → ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) → ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
21	4 20	eximii	⊢ ∃ 𝑥 ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) → ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) )
22	21	19.37iv	⊢ ( ( ( 1^st ‘ 𝐴 ) ⊆ Pg ∧ ( 2^nd ‘ 𝐴 ) ⊆ Pg ) → ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) )

Metamath Proof Explorer

Theorem elpglem2

Proof