Theorem elpwunsn

Description: Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007)

	Ref	Expression
Assertion	elpwunsn	⊢ ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) ↔ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) )
2		elpwg	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
3		dfss3	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
4	2 3	syl6bb	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝐴 ∈ 𝒫 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
5	4	notbid	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ¬ 𝐴 ∈ 𝒫 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
6	5	biimpa	⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
7		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
8	6 7	sylibr	⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
9		elpwi	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) )
10		ssel	⊢ ( 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) )
11		elun	⊢ ( 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) )
12		elsni	⊢ ( 𝑥 ∈ { 𝐶 } → 𝑥 = 𝐶 )
13	12	orim2i	⊢ ( ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) → ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐶 ) )
14	13	ord	⊢ ( ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) )
15	11 14	sylbi	⊢ ( 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) )
16	15	imim2i	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) ) )
17	16	impd	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
18	9 10 17	3syl	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
19		eleq1	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
20	19	biimpd	⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) )
21	18 20	syl6	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) ) )
22	21	expd	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) ) ) )
23	22	com4r	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) ) ) )
24	23	pm2.43b	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) ) )
25	24	rexlimdv	⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) )
26	25	imp	⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝐴 )
27	8 26	syldan	⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )
28	1 27	sylbi	⊢ ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )