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

Metamath Proof Explorer

Theorem acsfiindd

Description: In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in FaureFrolicher p. 83. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsfiindd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
acsfiindd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
acsfiindd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
acsfiindd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
Assertion acsfiindd ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 acsfiindd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2 acsfiindd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 acsfiindd.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 acsfiindd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
5 1 acsmred ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
6 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
7 simplr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑆 ∈ 𝐼 )
8 simpr ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) )
9 8 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑠 ∈ 𝒫 𝑆 )
10 9 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑠 ⊆ 𝑆 )
11 6 2 3 7 10 mrissmrid ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) ∧ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → 𝑠 ∈ 𝐼 )
12 11 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) → ∀ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑠 ∈ 𝐼 )
13 dfss3 ⊢ ( ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ↔ ∀ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑠 ∈ 𝐼 )
14 12 13 sylibr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝐼 ) → ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 )
15 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → 𝑆 ⊆ 𝑋 )
17 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) )
18 elfpw ⊢ ( 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ↔ ( 𝑡 ⊆ ( 𝑆 ∖ { 𝑥 } ) ∧ 𝑡 ∈ Fin ) )
19 17 18 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( 𝑡 ⊆ ( 𝑆 ∖ { 𝑥 } ) ∧ 𝑡 ∈ Fin ) )
20 19 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → 𝑡 ⊆ ( 𝑆 ∖ { 𝑥 } ) )
21 20 difss2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → 𝑡 ⊆ 𝑆 )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → 𝑥 ∈ 𝑆 )
23 22 snssd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → { 𝑥 } ⊆ 𝑆 )
24 21 23 unssd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( 𝑡 ∪ { 𝑥 } ) ⊆ 𝑆 )
25 19 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → 𝑡 ∈ Fin )
26 snfi ⊢ { 𝑥 } ∈ Fin
27 unfi ⊢ ( ( 𝑡 ∈ Fin ∧ { 𝑥 } ∈ Fin ) → ( 𝑡 ∪ { 𝑥 } ) ∈ Fin )
28 25 26 27 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( 𝑡 ∪ { 𝑥 } ) ∈ Fin )
29 elfpw ⊢ ( ( 𝑡 ∪ { 𝑥 } ) ∈ ( 𝒫 𝑆 ∩ Fin ) ↔ ( ( 𝑡 ∪ { 𝑥 } ) ⊆ 𝑆 ∧ ( 𝑡 ∪ { 𝑥 } ) ∈ Fin ) )
30 24 28 29 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( 𝑡 ∪ { 𝑥 } ) ∈ ( 𝒫 𝑆 ∩ Fin ) )
31 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
32 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → 𝑠 ∈ 𝐼 )
33 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑥 ∈ 𝑆 )
34 snidg ⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ { 𝑥 } )
35 elun2 ⊢ ( 𝑥 ∈ { 𝑥 } → 𝑥 ∈ ( 𝑡 ∪ { 𝑥 } ) )
36 33 34 35 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑡 ∪ { 𝑥 } ) )
37 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑠 = ( 𝑡 ∪ { 𝑥 } ) )
38 36 37 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑥 ∈ 𝑠 )
39 38 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → 𝑥 ∈ 𝑠 )
40 2 3 31 32 39 ismri2dad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) )
41 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
42 20 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑡 ⊆ ( 𝑆 ∖ { 𝑥 } ) )
43 neldifsnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ¬ 𝑥 ∈ ( 𝑆 ∖ { 𝑥 } ) )
44 42 43 ssneldd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ¬ 𝑥 ∈ 𝑡 )
45 difsnb ⊢ ( ¬ 𝑥 ∈ 𝑡 ↔ ( 𝑡 ∖ { 𝑥 } ) = 𝑡 )
46 44 45 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑡 ∖ { 𝑥 } ) = 𝑡 )
47 ssun1 ⊢ 𝑡 ⊆ ( 𝑡 ∪ { 𝑥 } )
48 47 37 sseqtrrid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑡 ⊆ 𝑠 )
49 48 ssdifd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑡 ∖ { 𝑥 } ) ⊆ ( 𝑠 ∖ { 𝑥 } ) )
50 46 49 eqsstrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑡 ⊆ ( 𝑠 ∖ { 𝑥 } ) )
51 24 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑡 ∪ { 𝑥 } ) ⊆ 𝑆 )
52 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑆 ⊆ 𝑋 )
53 51 52 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑡 ∪ { 𝑥 } ) ⊆ 𝑋 )
54 37 53 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → 𝑠 ⊆ 𝑋 )
55 54 ssdifssd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑠 ∖ { 𝑥 } ) ⊆ 𝑋 )
56 41 2 50 55 mrcssd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑁 ‘ 𝑡 ) ⊆ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) )
57 56 sseld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ) )
58 57 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ) )
59 40 58 mtod ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) ∧ 𝑠 ∈ 𝐼 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) )
60 59 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) ∧ 𝑠 = ( 𝑡 ∪ { 𝑥 } ) ) → ( 𝑠 ∈ 𝐼 → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
61 30 60 rspcimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( ∀ 𝑠 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑠 ∈ 𝐼 → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
62 13 61 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ) → ( ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
63 62 impancom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → ( 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) → ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
64 63 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → ∀ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) )
65 4 ssdifssd ⊢ ( 𝜑 → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
66 1 2 65 acsficl2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ∃ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
67 66 notbid ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ¬ ∃ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
68 ralnex ⊢ ( ∀ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ↔ ¬ ∃ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) )
69 67 68 bitr4di ⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ∀ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ∀ 𝑡 ∈ ( 𝒫 ( 𝑆 ∖ { 𝑥 } ) ∩ Fin ) ¬ 𝑥 ∈ ( 𝑁 ‘ 𝑡 ) ) )
71 64 70 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
72 71 an32s ⊢ ( ( ( 𝜑 ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
73 72 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
74 2 3 15 16 73 ismri2dd ⊢ ( ( 𝜑 ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) → 𝑆 ∈ 𝐼 )
75 14 74 impbida ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ( 𝒫 𝑆 ∩ Fin ) ⊆ 𝐼 ) )