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 
|- ( ph -> A e. ( ACS ` X ) )
acsfiindd.2 
|- N = ( mrCls ` A )
acsfiindd.3 
|- I = ( mrInd ` A )
acsfiindd.4 
|- ( ph -> S C_ X )
Assertion acsfiindd 
|- ( ph -> ( S e. I <-> ( ~P S i^i Fin ) C_ I ) )

Proof

Step Hyp Ref Expression
1 acsfiindd.1 
 |-  ( ph -> A e. ( ACS ` X ) )
2 acsfiindd.2 
 |-  N = ( mrCls ` A )
3 acsfiindd.3 
 |-  I = ( mrInd ` A )
4 acsfiindd.4 
 |-  ( ph -> S C_ X )
5 1 acsmred 
 |-  ( ph -> A e. ( Moore ` X ) )
6 5 ad2antrr 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> A e. ( Moore ` X ) )
7 simplr 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> S e. I )
8 simpr 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> s e. ( ~P S i^i Fin ) )
9 8 elin1d 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> s e. ~P S )
10 9 elpwid 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> s C_ S )
11 6 2 3 7 10 mrissmrid 
 |-  ( ( ( ph /\ S e. I ) /\ s e. ( ~P S i^i Fin ) ) -> s e. I )
12 11 ralrimiva 
 |-  ( ( ph /\ S e. I ) -> A. s e. ( ~P S i^i Fin ) s e. I )
13 dfss3 
 |-  ( ( ~P S i^i Fin ) C_ I <-> A. s e. ( ~P S i^i Fin ) s e. I )
14 12 13 sylibr 
 |-  ( ( ph /\ S e. I ) -> ( ~P S i^i Fin ) C_ I )
15 5 adantr 
 |-  ( ( ph /\ ( ~P S i^i Fin ) C_ I ) -> A e. ( Moore ` X ) )
16 4 adantr 
 |-  ( ( ph /\ ( ~P S i^i Fin ) C_ I ) -> S C_ X )
17 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> t e. ( ~P ( S \ { x } ) i^i Fin ) )
18 elfpw 
 |-  ( t e. ( ~P ( S \ { x } ) i^i Fin ) <-> ( t C_ ( S \ { x } ) /\ t e. Fin ) )
19 17 18 sylib 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( t C_ ( S \ { x } ) /\ t e. Fin ) )
20 19 simpld 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> t C_ ( S \ { x } ) )
21 20 difss2d 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> t C_ S )
22 simplr 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> x e. S )
23 22 snssd 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> { x } C_ S )
24 21 23 unssd 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( t u. { x } ) C_ S )
25 19 simprd 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> t e. Fin )
26 snfi 
 |-  { x } e. Fin
27 unfi 
 |-  ( ( t e. Fin /\ { x } e. Fin ) -> ( t u. { x } ) e. Fin )
28 25 26 27 sylancl 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( t u. { x } ) e. Fin )
29 elfpw 
 |-  ( ( t u. { x } ) e. ( ~P S i^i Fin ) <-> ( ( t u. { x } ) C_ S /\ ( t u. { x } ) e. Fin ) )
30 24 28 29 sylanbrc 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( t u. { x } ) e. ( ~P S i^i Fin ) )
31 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> A e. ( Moore ` X ) )
32 simpr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> s e. I )
33 simpllr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> x e. S )
34 snidg 
 |-  ( x e. S -> x e. { x } )
35 elun2 
 |-  ( x e. { x } -> x e. ( t u. { x } ) )
36 33 34 35 3syl 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> x e. ( t u. { x } ) )
37 simpr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> s = ( t u. { x } ) )
38 36 37 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> x e. s )
39 38 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> x e. s )
40 2 3 31 32 39 ismri2dad 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> -. x e. ( N ` ( s \ { x } ) ) )
41 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> A e. ( Moore ` X ) )
42 20 adantr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> t C_ ( S \ { x } ) )
43 neldifsnd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> -. x e. ( S \ { x } ) )
44 42 43 ssneldd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> -. x e. t )
45 difsnb 
 |-  ( -. x e. t <-> ( t \ { x } ) = t )
46 44 45 sylib 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( t \ { x } ) = t )
47 ssun1 
 |-  t C_ ( t u. { x } )
48 47 37 sseqtrrid 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> t C_ s )
49 48 ssdifd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( t \ { x } ) C_ ( s \ { x } ) )
50 46 49 eqsstrrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> t C_ ( s \ { x } ) )
51 24 adantr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( t u. { x } ) C_ S )
52 4 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> S C_ X )
53 51 52 sstrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( t u. { x } ) C_ X )
54 37 53 eqsstrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> s C_ X )
55 54 ssdifssd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( s \ { x } ) C_ X )
56 41 2 50 55 mrcssd 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( N ` t ) C_ ( N ` ( s \ { x } ) ) )
57 56 sseld 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( x e. ( N ` t ) -> x e. ( N ` ( s \ { x } ) ) ) )
58 57 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> ( x e. ( N ` t ) -> x e. ( N ` ( s \ { x } ) ) ) )
59 40 58 mtod 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) /\ s e. I ) -> -. x e. ( N ` t ) )
60 59 ex 
 |-  ( ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) /\ s = ( t u. { x } ) ) -> ( s e. I -> -. x e. ( N ` t ) ) )
61 30 60 rspcimdv 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( A. s e. ( ~P S i^i Fin ) s e. I -> -. x e. ( N ` t ) ) )
62 13 61 syl5bi 
 |-  ( ( ( ph /\ x e. S ) /\ t e. ( ~P ( S \ { x } ) i^i Fin ) ) -> ( ( ~P S i^i Fin ) C_ I -> -. x e. ( N ` t ) ) )
63 62 impancom 
 |-  ( ( ( ph /\ x e. S ) /\ ( ~P S i^i Fin ) C_ I ) -> ( t e. ( ~P ( S \ { x } ) i^i Fin ) -> -. x e. ( N ` t ) ) )
64 63 ralrimiv 
 |-  ( ( ( ph /\ x e. S ) /\ ( ~P S i^i Fin ) C_ I ) -> A. t e. ( ~P ( S \ { x } ) i^i Fin ) -. x e. ( N ` t ) )
65 4 ssdifssd 
 |-  ( ph -> ( S \ { x } ) C_ X )
66 1 2 65 acsficl2d 
 |-  ( ph -> ( x e. ( N ` ( S \ { x } ) ) <-> E. t e. ( ~P ( S \ { x } ) i^i Fin ) x e. ( N ` t ) ) )
67 66 notbid 
 |-  ( ph -> ( -. x e. ( N ` ( S \ { x } ) ) <-> -. E. t e. ( ~P ( S \ { x } ) i^i Fin ) x e. ( N ` t ) ) )
68 ralnex 
 |-  ( A. t e. ( ~P ( S \ { x } ) i^i Fin ) -. x e. ( N ` t ) <-> -. E. t e. ( ~P ( S \ { x } ) i^i Fin ) x e. ( N ` t ) )
69 67 68 bitr4di 
 |-  ( ph -> ( -. x e. ( N ` ( S \ { x } ) ) <-> A. t e. ( ~P ( S \ { x } ) i^i Fin ) -. x e. ( N ` t ) ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ ( ~P S i^i Fin ) C_ I ) -> ( -. x e. ( N ` ( S \ { x } ) ) <-> A. t e. ( ~P ( S \ { x } ) i^i Fin ) -. x e. ( N ` t ) ) )
71 64 70 mpbird 
 |-  ( ( ( ph /\ x e. S ) /\ ( ~P S i^i Fin ) C_ I ) -> -. x e. ( N ` ( S \ { x } ) ) )
72 71 an32s 
 |-  ( ( ( ph /\ ( ~P S i^i Fin ) C_ I ) /\ x e. S ) -> -. x e. ( N ` ( S \ { x } ) ) )
73 72 ralrimiva 
 |-  ( ( ph /\ ( ~P S i^i Fin ) C_ I ) -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
74 2 3 15 16 73 ismri2dd 
 |-  ( ( ph /\ ( ~P S i^i Fin ) C_ I ) -> S e. I )
75 14 74 impbida 
 |-  ( ph -> ( S e. I <-> ( ~P S i^i Fin ) C_ I ) )