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

Metamath Proof Explorer

Theorem fin1a2s

Description: An II-infinite set can have an I-infinite part broken off and remain II-infinite. (Contributed by Stefan O'Rear, 8-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin1a2s 
|- ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> A e. Fin2 )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( c e. ~P ~P A -> c C_ ~P A )
2 fin12 
 |-  ( x e. Fin -> x e. Fin2 )
3 fin23 
 |-  ( x e. Fin2 -> x e. Fin3 )
4 2 3 syl 
 |-  ( x e. Fin -> x e. Fin3 )
5 fin23 
 |-  ( ( A \ x ) e. Fin2 -> ( A \ x ) e. Fin3 )
6 4 5 orim12i 
 |-  ( ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> ( x e. Fin3 \/ ( A \ x ) e. Fin3 ) )
7 6 ralimi 
 |-  ( A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> A. x e. ~P A ( x e. Fin3 \/ ( A \ x ) e. Fin3 ) )
8 fin1a2lem8 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin3 \/ ( A \ x ) e. Fin3 ) ) -> A e. Fin3 )
9 7 8 sylan2 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> A e. Fin3 )
10 9 adantr 
 |-  ( ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) -> A e. Fin3 )
11 simplrl 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> c C_ ~P A )
12 simprrr 
 |-  ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) -> [C.] Or c )
13 12 adantr 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> [C.] Or c )
14 simprl 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> -. U. c e. c )
15 simplrl 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> c C_ ~P A )
16 ssralv 
 |-  ( c C_ ~P A -> ( A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> A. x e. c ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) )
17 15 16 syl 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> ( A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> A. x e. c ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) )
18 idd 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ x e. c ) -> ( x e. Fin -> x e. Fin ) )
19 fin1a2lem13 
 |-  ( ( ( c C_ ~P A /\ [C.] Or c /\ -. U. c e. c ) /\ ( -. x e. Fin /\ x e. c ) ) -> -. ( A \ x ) e. Fin2 )
20 19 ex 
 |-  ( ( c C_ ~P A /\ [C.] Or c /\ -. U. c e. c ) -> ( ( -. x e. Fin /\ x e. c ) -> -. ( A \ x ) e. Fin2 ) )
21 20 3expa 
 |-  ( ( ( c C_ ~P A /\ [C.] Or c ) /\ -. U. c e. c ) -> ( ( -. x e. Fin /\ x e. c ) -> -. ( A \ x ) e. Fin2 ) )
22 21 adantlrl 
 |-  ( ( ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) /\ -. U. c e. c ) -> ( ( -. x e. Fin /\ x e. c ) -> -. ( A \ x ) e. Fin2 ) )
23 22 adantll 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> ( ( -. x e. Fin /\ x e. c ) -> -. ( A \ x ) e. Fin2 ) )
24 23 imp 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ ( -. x e. Fin /\ x e. c ) ) -> -. ( A \ x ) e. Fin2 )
25 24 ancom2s 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ ( x e. c /\ -. x e. Fin ) ) -> -. ( A \ x ) e. Fin2 )
26 25 expr 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ x e. c ) -> ( -. x e. Fin -> -. ( A \ x ) e. Fin2 ) )
27 26 con4d 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ x e. c ) -> ( ( A \ x ) e. Fin2 -> x e. Fin ) )
28 18 27 jaod 
 |-  ( ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) /\ x e. c ) -> ( ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> x e. Fin ) )
29 28 ralimdva 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> ( A. x e. c ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> A. x e. c x e. Fin ) )
30 17 29 syld 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> ( A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> A. x e. c x e. Fin ) )
31 30 impr 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> A. x e. c x e. Fin )
32 dfss3 
 |-  ( c C_ Fin <-> A. x e. c x e. Fin )
33 31 32 sylibr 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> c C_ Fin )
34 simprrl 
 |-  ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) -> c =/= (/) )
35 34 adantr 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> c =/= (/) )
36 fin1a2lem12 
 |-  ( ( ( c C_ ~P A /\ [C.] Or c /\ -. U. c e. c ) /\ ( c C_ Fin /\ c =/= (/) ) ) -> -. A e. Fin3 )
37 11 13 14 33 35 36 syl32anc 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ ( -. U. c e. c /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) ) -> -. A e. Fin3 )
38 37 expr 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ -. U. c e. c ) -> ( A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) -> -. A e. Fin3 ) )
39 38 impancom 
 |-  ( ( ( A e. V /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> ( -. U. c e. c -> -. A e. Fin3 ) )
40 39 an32s 
 |-  ( ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) -> ( -. U. c e. c -> -. A e. Fin3 ) )
41 10 40 mt4d 
 |-  ( ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) /\ ( c C_ ~P A /\ ( c =/= (/) /\ [C.] Or c ) ) ) -> U. c e. c )
42 41 exp32 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> ( c C_ ~P A -> ( ( c =/= (/) /\ [C.] Or c ) -> U. c e. c ) ) )
43 1 42 syl5 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> ( c e. ~P ~P A -> ( ( c =/= (/) /\ [C.] Or c ) -> U. c e. c ) ) )
44 43 ralrimiv 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> A. c e. ~P ~P A ( ( c =/= (/) /\ [C.] Or c ) -> U. c e. c ) )
45 isfin2 
 |-  ( A e. V -> ( A e. Fin2 <-> A. c e. ~P ~P A ( ( c =/= (/) /\ [C.] Or c ) -> U. c e. c ) ) )
46 45 adantr 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> ( A e. Fin2 <-> A. c e. ~P ~P A ( ( c =/= (/) /\ [C.] Or c ) -> U. c e. c ) ) )
47 44 46 mpbird 
 |-  ( ( A e. V /\ A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin2 ) ) -> A e. Fin2 )