elpglem2 - Mathbox for Emmett Weisz

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

Theorem elpglem2 50523

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

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

Distinct variable group: 𝑥,𝐴

**Proof of Theorem elpglem2**
Step	Hyp	Ref	Expression
1		fvex 6898	. . . . 5 ⊢ (1^st ‘𝐴) ∈ V
2		fvex 6898	. . . . 5 ⊢ (2^nd ‘𝐴) ∈ V
3	1, 2	unex 7748	. . . 4 ⊢ ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) ∈ V
4	3	isseti 3475	. . 3 ⊢ ∃𝑥 𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴))
5		sseq1 3963	. . . . . 6 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (𝑥 ⊆ Pg ↔ ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) ⊆ Pg))
6		unss 4143	. . . . . 6 ⊢ (((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg) ↔ ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) ⊆ Pg)
7	5, 6	bitr4di 292	. . . . 5 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (𝑥 ⊆ Pg ↔ ((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg)))
8	7	biimprd 251	. . . 4 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg) → 𝑥 ⊆ Pg))
9		ssun1 4131	. . . . . . 7 ⊢ (1^st ‘𝐴) ⊆ ((1^st ‘𝐴) ∪ (2^nd ‘𝐴))
10		id 23	. . . . . . 7 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → 𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)))
11	9, 10	sseqtrrid 3981	. . . . . 6 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (1^st ‘𝐴) ⊆ 𝑥)
12		vex 3461	. . . . . . 7 ⊢ 𝑥 ∈ V
13	12	elpw2 5307	. . . . . 6 ⊢ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ↔ (1^st ‘𝐴) ⊆ 𝑥)
14	11, 13	sylibr 237	. . . . 5 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (1^st ‘𝐴) ∈ 𝒫 𝑥)
15		ssun2 4132	. . . . . . 7 ⊢ (2^nd ‘𝐴) ⊆ ((1^st ‘𝐴) ∪ (2^nd ‘𝐴))
16	15, 10	sseqtrrid 3981	. . . . . 6 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (2^nd ‘𝐴) ⊆ 𝑥)
17	12	elpw2 5307	. . . . . 6 ⊢ ((2^nd ‘𝐴) ∈ 𝒫 𝑥 ↔ (2^nd ‘𝐴) ⊆ 𝑥)
18	16, 17	sylibr 237	. . . . 5 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (2^nd ‘𝐴) ∈ 𝒫 𝑥)
19	14, 18	jca 521	. . . 4 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥))
20	8, 19	jctird 536	. . 3 ⊢ (𝑥 = ((1^st ‘𝐴) ∪ (2^nd ‘𝐴)) → (((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg) → (𝑥 ⊆ Pg ∧ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥))))
21	4, 20	eximii 1870	. 2 ⊢ ∃𝑥(((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg) → (𝑥 ⊆ Pg ∧ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥)))
22	21	19.37iv 1981	1 ⊢ (((1^st ‘𝐴) ⊆ Pg ∧ (2^nd ‘𝐴) ⊆ Pg) → ∃𝑥(𝑥 ⊆ Pg ∧ ((1^st ‘𝐴) ∈ 𝒫 𝑥 ∧ (2^nd ‘𝐴) ∈ 𝒫 𝑥)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2146 ∪ cun 3904 ⊆ wss 3906 𝒫 cpw 4564 ‘cfv 6540 1^st c1st 7986 2^nd c2nd 7987 Pgcpg 50520

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pr 5406 ax-un 7738

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-pw 4566 df-sn 4592 df-pr 4594 df-uni 4875 df-iota 6496 df-fv 6548

This theorem is used by: elpg 50525

W3C validator