Metamath Proof Explorer

Theorem ssfin4

Description: Dedekind finite sets have Dedekind finite subsets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 6-May-2015) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion ssfin4 
|- ( ( A e. Fin4 /\ B C_ A ) -> B e. Fin4 )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> A e. Fin4 )
2 pssss 
 |-  ( x C. B -> x C_ B )
3 simpr 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> B C_ A )
4 2 3 sylan9ssr 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> x C_ A )
5 difssd 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> ( A \ B ) C_ A )
6 4 5 unssd 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> ( x u. ( A \ B ) ) C_ A )
7 pssnel 
 |-  ( x C. B -> E. c ( c e. B /\ -. c e. x ) )
8 7 adantl 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> E. c ( c e. B /\ -. c e. x ) )
9 simpllr 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> B C_ A )
10 simprl 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> c e. B )
11 9 10 sseldd 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> c e. A )
12 simprr 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> -. c e. x )
13 elndif 
 |-  ( c e. B -> -. c e. ( A \ B ) )
14 13 ad2antrl 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> -. c e. ( A \ B ) )
15 ioran 
 |-  ( -. ( c e. x \/ c e. ( A \ B ) ) <-> ( -. c e. x /\ -. c e. ( A \ B ) ) )
16 elun 
 |-  ( c e. ( x u. ( A \ B ) ) <-> ( c e. x \/ c e. ( A \ B ) ) )
17 15 16 xchnxbir 
 |-  ( -. c e. ( x u. ( A \ B ) ) <-> ( -. c e. x /\ -. c e. ( A \ B ) ) )
18 12 14 17 sylanbrc 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> -. c e. ( x u. ( A \ B ) ) )
19 nelneq2 
 |-  ( ( c e. A /\ -. c e. ( x u. ( A \ B ) ) ) -> -. A = ( x u. ( A \ B ) ) )
20 11 18 19 syl2anc 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> -. A = ( x u. ( A \ B ) ) )
21 eqcom 
 |-  ( A = ( x u. ( A \ B ) ) <-> ( x u. ( A \ B ) ) = A )
22 20 21 sylnib 
 |-  ( ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) /\ ( c e. B /\ -. c e. x ) ) -> -. ( x u. ( A \ B ) ) = A )
23 8 22 exlimddv 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> -. ( x u. ( A \ B ) ) = A )
24 dfpss2 
 |-  ( ( x u. ( A \ B ) ) C. A <-> ( ( x u. ( A \ B ) ) C_ A /\ -. ( x u. ( A \ B ) ) = A ) )
25 6 23 24 sylanbrc 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ x C. B ) -> ( x u. ( A \ B ) ) C. A )
26 25 adantrr 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( x u. ( A \ B ) ) C. A )
27 simprr 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> x ~~ B )
28 difexg 
 |-  ( A e. Fin4 -> ( A \ B ) e. _V )
29 enrefg 
 |-  ( ( A \ B ) e. _V -> ( A \ B ) ~~ ( A \ B ) )
30 1 28 29 3syl 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( A \ B ) ~~ ( A \ B ) )
31 2 ad2antrl 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> x C_ B )
32 ssinss1 
 |-  ( x C_ B -> ( x i^i A ) C_ B )
33 31 32 syl 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( x i^i A ) C_ B )
34 inssdif0 
 |-  ( ( x i^i A ) C_ B <-> ( x i^i ( A \ B ) ) = (/) )
35 33 34 sylib 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( x i^i ( A \ B ) ) = (/) )
36 disjdif 
 |-  ( B i^i ( A \ B ) ) = (/)
37 35 36 jctir 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( ( x i^i ( A \ B ) ) = (/) /\ ( B i^i ( A \ B ) ) = (/) ) )
38 unen 
 |-  ( ( ( x ~~ B /\ ( A \ B ) ~~ ( A \ B ) ) /\ ( ( x i^i ( A \ B ) ) = (/) /\ ( B i^i ( A \ B ) ) = (/) ) ) -> ( x u. ( A \ B ) ) ~~ ( B u. ( A \ B ) ) )
39 27 30 37 38 syl21anc 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( x u. ( A \ B ) ) ~~ ( B u. ( A \ B ) ) )
40 simplr 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> B C_ A )
41 undif 
 |-  ( B C_ A <-> ( B u. ( A \ B ) ) = A )
42 40 41 sylib 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( B u. ( A \ B ) ) = A )
43 39 42 breqtrd 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> ( x u. ( A \ B ) ) ~~ A )
44 fin4i 
 |-  ( ( ( x u. ( A \ B ) ) C. A /\ ( x u. ( A \ B ) ) ~~ A ) -> -. A e. Fin4 )
45 26 43 44 syl2anc 
 |-  ( ( ( A e. Fin4 /\ B C_ A ) /\ ( x C. B /\ x ~~ B ) ) -> -. A e. Fin4 )
46 1 45 pm2.65da 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> -. ( x C. B /\ x ~~ B ) )
47 46 nexdv 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> -. E. x ( x C. B /\ x ~~ B ) )
48 ssexg 
 |-  ( ( B C_ A /\ A e. Fin4 ) -> B e. _V )
49 48 ancoms 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> B e. _V )
50 isfin4 
 |-  ( B e. _V -> ( B e. Fin4 <-> -. E. x ( x C. B /\ x ~~ B ) ) )
51 49 50 syl 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> ( B e. Fin4 <-> -. E. x ( x C. B /\ x ~~ B ) ) )
52 47 51 mpbird 
 |-  ( ( A e. Fin4 /\ B C_ A ) -> B e. Fin4 )