Theorem fin23lem7

Description: Lemma for isfin2-2 . The componentwise complement of a nonempty collection of sets is nonempty. (Contributed by Stefan O'Rear, 31-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	fin23lem7	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
2		difss	⊢ ( 𝐴 ∖ 𝑦 ) ⊆ 𝐴
3		elpw2g	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ 𝑦 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑦 ) ⊆ 𝐴 ) )
4	3	ad2antrr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐴 ∖ 𝑦 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑦 ) ⊆ 𝐴 ) )
5	2 4	mpbiri	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ∖ 𝑦 ) ∈ 𝒫 𝐴 )
6		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) → 𝐵 ⊆ 𝒫 𝐴 )
7	6	sselda	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝒫 𝐴 )
8	7	elpwid	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ 𝐴 )
9		dfss4	⊢ ( 𝑦 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 )
10	8 9	sylib	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) = 𝑦 )
11		simpr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
12	10 11	eqeltrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ∈ 𝐵 )
13		difeq2	⊢ ( 𝑥 = ( 𝐴 ∖ 𝑦 ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) )
14	13	eleq1d	⊢ ( 𝑥 = ( 𝐴 ∖ 𝑦 ) → ( ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ∈ 𝐵 ) )
15	14	rspcev	⊢ ( ( ( 𝐴 ∖ 𝑦 ) ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ ( 𝐴 ∖ 𝑦 ) ) ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
16	5 12 15	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
17	16	ex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) )
18	17	exlimdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) )
19	1 18	biimtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ) → ( 𝐵 ≠ ∅ → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 ) )
20	19	3impia	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅ ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
21		rabn0	⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 )
22	20 21	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 } ≠ ∅ )