elpglem1 - Mathbox for Emmett Weisz

	Mathbox for Emmett Weisz		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elpglem1		Structured version Visualization version GIF version

Theorem elpglem1 46087

Description: Lemma for elpg 46090. (Contributed by Emmett Weisz, 28-Aug-2021.)

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

Distinct variable group: 𝑥,𝐴

**Proof of Theorem elpglem1**
Step	Hyp	Ref	Expression
1		elpwi 4522	. . . . 5 ⊢ ((1^st ‘𝐴) ∈ 𝒫 𝑥 → (1^st ‘𝐴) ⊆ 𝑥)
2	1	adantl 485	. . . 4 ⊢ ((𝑥 ⊆ Pg ∧ (1^st ‘𝐴) ∈ 𝒫 𝑥) → (1^st ‘𝐴) ⊆ 𝑥)
3		simpl 486	. . . 4 ⊢ ((𝑥 ⊆ Pg ∧ (1^st ‘𝐴) ∈ 𝒫 𝑥) → 𝑥 ⊆ Pg)
4	2, 3	sstrd 3911	. . 3 ⊢ ((𝑥 ⊆ Pg ∧ (1^st ‘𝐴) ∈ 𝒫 𝑥) → (1^st ‘𝐴) ⊆ Pg)
5		elpwi 4522	. . . . 5 ⊢ ((2^nd ‘𝐴) ∈ 𝒫 𝑥 → (2^nd ‘𝐴) ⊆ 𝑥)
6	5	adantl 485	. . . 4 ⊢ ((𝑥 ⊆ Pg ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥) → (2^nd ‘𝐴) ⊆ 𝑥)
7		simpl 486	. . . 4 ⊢ ((𝑥 ⊆ Pg ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥) → 𝑥 ⊆ Pg)
8	6, 7	sstrd 3911	. . 3 ⊢ ((𝑥 ⊆ Pg ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥) → (2^nd ‘𝐴) ⊆ Pg)
9	4, 8	anim12dan 622	. 2 ⊢ ((𝑥 ⊆ Pg ∧ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥)) → ((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg))
10	9	exlimiv 1938	1 ⊢ (∃𝑥(𝑥 ⊆ Pg ∧ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥)) → ((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∃wex 1787 ∈ wcel 2110 ⊆ wss 3866 𝒫 cpw 4513 ‘cfv 6380 1^st c1st 7759 2^nd c2nd 7760 Pgcpg 46085

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708

This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-pw 4515

This theorem is referenced by: elpg 46090