This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝒫 𝐴 ∧ 𝐵 ≠ ∅ ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑥 ) ∈ 𝐵 } ≠ ∅ )