Metamath Proof Explorer

Theorem isf34lem4

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion isf34lem4 ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ 𝑋 ) = ∩ ( 𝐹 “ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2 sspwuni ⊢ ( 𝑋 ⊆ 𝒫 𝐴 ↔ ∪ 𝑋 ⊆ 𝐴 )
3 1 isf34lem1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑋 ⊆ 𝐴 ) → ( 𝐹 ‘ ∪ 𝑋 ) = ( 𝐴 ∖ ∪ 𝑋 ) )
4 2 3 sylan2b ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 ‘ ∪ 𝑋 ) = ( 𝐴 ∖ ∪ 𝑋 ) )
5 4 adantrr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ 𝑋 ) = ( 𝐴 ∖ ∪ 𝑋 ) )
6 simplrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) → ¬ 𝑏 ∈ ∪ 𝑋 )
7 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) → 𝑏 ∈ 𝐴 )
8 7 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) ∧ ¬ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 )
9 simpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) ∧ ¬ 𝑏 ∈ 𝑎 ) → ¬ 𝑏 ∈ 𝑎 )
10 8 9 eldifd ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) ∧ ¬ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ ( 𝐴 ∖ 𝑎 ) )
11 simplrr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) ∧ ¬ 𝑏 ∈ 𝑎 ) → ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 )
12 elunii ⊢ ( ( 𝑏 ∈ ( 𝐴 ∖ 𝑎 ) ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) → 𝑏 ∈ ∪ 𝑋 )
13 10 11 12 syl2anc ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) ∧ ¬ 𝑏 ∈ 𝑎 ) → 𝑏 ∈ ∪ 𝑋 )
14 13 ex ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) → ( ¬ 𝑏 ∈ 𝑎 → 𝑏 ∈ ∪ 𝑋 ) )
15 6 14 mt3d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ) ) → 𝑏 ∈ 𝑎 )
16 15 expr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) ∧ 𝑎 ∈ 𝒫 𝐴 ) → ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
17 16 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) → ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
18 17 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) → ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ) )
19 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑐 𝑐 ∈ 𝑋 )
20 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → 𝑋 ⊆ 𝒫 𝐴 )
21 20 sselda ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → 𝑐 ∈ 𝒫 𝐴 )
22 21 elpwid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → 𝑐 ⊆ 𝐴 )
23 dfss4 ⊢ ( 𝑐 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) = 𝑐 )
24 22 23 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) = 𝑐 )
25 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → 𝑐 ∈ 𝑋 )
26 24 25 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 )
27 difss ⊢ ( 𝐴 ∖ 𝑐 ) ⊆ 𝐴
28 elpw2g ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 ↔ ( 𝐴 ∖ 𝑐 ) ⊆ 𝐴 ) )
29 27 28 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 )
30 29 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 )
31 difeq2 ⊢ ( 𝑎 = ( 𝐴 ∖ 𝑐 ) → ( 𝐴 ∖ 𝑎 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) )
32 31 eleq1d ⊢ ( 𝑎 = ( 𝐴 ∖ 𝑐 ) → ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 ) )
33 eleq2 ⊢ ( 𝑎 = ( 𝐴 ∖ 𝑐 ) → ( 𝑏 ∈ 𝑎 ↔ 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) )
34 32 33 imbi12d ⊢ ( 𝑎 = ( 𝐴 ∖ 𝑐 ) → ( ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ↔ ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) ) )
35 34 rspcv ⊢ ( ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) ) )
36 30 35 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) ) )
37 26 36 mpid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) )
38 eldifi ⊢ ( 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) → 𝑏 ∈ 𝐴 )
39 37 38 syl6 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) ∧ 𝑐 ∈ 𝑋 ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 ) )
40 39 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝑐 ∈ 𝑋 → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 ) ) )
41 40 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( ∃ 𝑐 𝑐 ∈ 𝑋 → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 ) ) )
42 19 41 syl5bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝑋 ≠ ∅ → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 ) ) )
43 42 impr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → 𝑏 ∈ 𝐴 ) )
44 eluni ⊢ ( 𝑏 ∈ ∪ 𝑋 ↔ ∃ 𝑐 ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) )
45 29 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 )
46 26 adantlrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ 𝑐 ∈ 𝑋 ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 )
47 46 adantrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 )
48 elndif ⊢ ( 𝑏 ∈ 𝑐 → ¬ 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) )
49 48 ad2antrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ¬ 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) )
50 47 49 jcnd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ¬ ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) )
51 34 notbid ⊢ ( 𝑎 = ( 𝐴 ∖ 𝑐 ) → ( ¬ ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ↔ ¬ ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) ) )
52 51 rspcev ⊢ ( ( ( 𝐴 ∖ 𝑐 ) ∈ 𝒫 𝐴 ∧ ¬ ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑐 ) ) ∈ 𝑋 → 𝑏 ∈ ( 𝐴 ∖ 𝑐 ) ) ) → ∃ 𝑎 ∈ 𝒫 𝐴 ¬ ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
53 45 50 52 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ∃ 𝑎 ∈ 𝒫 𝐴 ¬ ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
54 rexnal ⊢ ( ∃ 𝑎 ∈ 𝒫 𝐴 ¬ ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ↔ ¬ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
55 53 54 sylib ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) ∧ ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) ) → ¬ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
56 55 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) → ¬ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ) )
57 56 exlimdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∃ 𝑐 ( 𝑏 ∈ 𝑐 ∧ 𝑐 ∈ 𝑋 ) → ¬ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ) )
58 44 57 syl5bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝑏 ∈ ∪ 𝑋 → ¬ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ) )
59 58 con2d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → ¬ 𝑏 ∈ ∪ 𝑋 ) )
60 43 59 jcad ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) → ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ) )
61 18 60 impbid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) ) )
62 eldif ⊢ ( 𝑏 ∈ ( 𝐴 ∖ ∪ 𝑋 ) ↔ ( 𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ ∪ 𝑋 ) )
63 vex ⊢ 𝑏 ∈ V
64 63 elintrab ⊢ ( 𝑏 ∈ ∩ { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 } ↔ ∀ 𝑎 ∈ 𝒫 𝐴 ( ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 → 𝑏 ∈ 𝑎 ) )
65 61 62 64 3bitr4g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝑏 ∈ ( 𝐴 ∖ ∪ 𝑋 ) ↔ 𝑏 ∈ ∩ { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 } ) )
66 65 eqrdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐴 ∖ ∪ 𝑋 ) = ∩ { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 } )
67 5 66 eqtrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ 𝑋 ) = ∩ { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 } )
68 1 compss ⊢ ( 𝐹 “ 𝑋 ) = { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 }
69 68 inteqi ⊢ ∩ ( 𝐹 “ 𝑋 ) = ∩ { 𝑎 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑎 ) ∈ 𝑋 }
70 67 69 eqtr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ⊆ 𝒫 𝐴 ∧ 𝑋 ≠ ∅ ) ) → ( 𝐹 ‘ ∪ 𝑋 ) = ∩ ( 𝐹 “ 𝑋 ) )