Metamath Proof Explorer

Theorem fin2so

Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019)

Ref Expression
Assertion fin2so 
|- ( ( A e. Fin2 /\ R Or A ) -> A e. Fin )

Proof

Step Hyp Ref Expression
1 simplll 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> A e. Fin2 )
2 ssrab2 
 |-  { w e. x | w R v } C_ x
3 sstr 
 |-  ( ( { w e. x | w R v } C_ x /\ x C_ A ) -> { w e. x | w R v } C_ A )
4 2 3 mpan 
 |-  ( x C_ A -> { w e. x | w R v } C_ A )
5 elpw2g 
 |-  ( A e. Fin2 -> ( { w e. x | w R v } e. ~P A <-> { w e. x | w R v } C_ A ) )
6 5 biimpar 
 |-  ( ( A e. Fin2 /\ { w e. x | w R v } C_ A ) -> { w e. x | w R v } e. ~P A )
7 4 6 sylan2 
 |-  ( ( A e. Fin2 /\ x C_ A ) -> { w e. x | w R v } e. ~P A )
8 7 ralrimivw 
 |-  ( ( A e. Fin2 /\ x C_ A ) -> A. v e. x { w e. x | w R v } e. ~P A )
9 vex 
 |-  x e. _V
10 9 rabex 
 |-  { w e. x | w R v } e. _V
11 10 rgenw 
 |-  A. v e. x { w e. x | w R v } e. _V
12 eqid 
 |-  ( v e. x |-> { w e. x | w R v } ) = ( v e. x |-> { w e. x | w R v } )
13 eleq1 
 |-  ( y = { w e. x | w R v } -> ( y e. ~P A <-> { w e. x | w R v } e. ~P A ) )
14 12 13 ralrnmptw 
 |-  ( A. v e. x { w e. x | w R v } e. _V -> ( A. y e. ran ( v e. x |-> { w e. x | w R v } ) y e. ~P A <-> A. v e. x { w e. x | w R v } e. ~P A ) )
15 11 14 ax-mp 
 |-  ( A. y e. ran ( v e. x |-> { w e. x | w R v } ) y e. ~P A <-> A. v e. x { w e. x | w R v } e. ~P A )
16 8 15 sylibr 
 |-  ( ( A e. Fin2 /\ x C_ A ) -> A. y e. ran ( v e. x |-> { w e. x | w R v } ) y e. ~P A )
17 dfss3 
 |-  ( ran ( v e. x |-> { w e. x | w R v } ) C_ ~P A <-> A. y e. ran ( v e. x |-> { w e. x | w R v } ) y e. ~P A )
18 16 17 sylibr 
 |-  ( ( A e. Fin2 /\ x C_ A ) -> ran ( v e. x |-> { w e. x | w R v } ) C_ ~P A )
19 18 adantlr 
 |-  ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) -> ran ( v e. x |-> { w e. x | w R v } ) C_ ~P A )
20 19 adantr 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> ran ( v e. x |-> { w e. x | w R v } ) C_ ~P A )
21 10 12 dmmpti 
 |-  dom ( v e. x |-> { w e. x | w R v } ) = x
22 21 neeq1i 
 |-  ( dom ( v e. x |-> { w e. x | w R v } ) =/= (/) <-> x =/= (/) )
23 dm0rn0 
 |-  ( dom ( v e. x |-> { w e. x | w R v } ) = (/) <-> ran ( v e. x |-> { w e. x | w R v } ) = (/) )
24 23 necon3bii 
 |-  ( dom ( v e. x |-> { w e. x | w R v } ) =/= (/) <-> ran ( v e. x |-> { w e. x | w R v } ) =/= (/) )
25 22 24 sylbb1 
 |-  ( x =/= (/) -> ran ( v e. x |-> { w e. x | w R v } ) =/= (/) )
26 25 adantl 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> ran ( v e. x |-> { w e. x | w R v } ) =/= (/) )
27 soss 
 |-  ( x C_ A -> ( R Or A -> R Or x ) )
28 27 impcom 
 |-  ( ( R Or A /\ x C_ A ) -> R Or x )
29 porpss 
 |-  [C.] Po ran ( v e. x |-> { w e. x | w R v } )
30 29 a1i 
 |-  ( R Or x -> [C.] Po ran ( v e. x |-> { w e. x | w R v } ) )
31 solin 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( v R y \/ v = y \/ y R v ) )
32 fin2solem 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( v R y -> { w e. x | w R v } [C.] { w e. x | w R y } ) )
33 breq2 
 |-  ( v = y -> ( w R v <-> w R y ) )
34 33 rabbidv 
 |-  ( v = y -> { w e. x | w R v } = { w e. x | w R y } )
35 34 a1i 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( v = y -> { w e. x | w R v } = { w e. x | w R y } ) )
36 fin2solem 
 |-  ( ( R Or x /\ ( y e. x /\ v e. x ) ) -> ( y R v -> { w e. x | w R y } [C.] { w e. x | w R v } ) )
37 36 ancom2s 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( y R v -> { w e. x | w R y } [C.] { w e. x | w R v } ) )
38 32 35 37 3orim123d 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( ( v R y \/ v = y \/ y R v ) -> ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) ) )
39 31 38 mpd 
 |-  ( ( R Or x /\ ( v e. x /\ y e. x ) ) -> ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) )
40 39 ralrimivva 
 |-  ( R Or x -> A. v e. x A. y e. x ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) )
41 breq1 
 |-  ( u = { w e. x | w R v } -> ( u [C.] { w e. x | w R y } <-> { w e. x | w R v } [C.] { w e. x | w R y } ) )
42 eqeq1 
 |-  ( u = { w e. x | w R v } -> ( u = { w e. x | w R y } <-> { w e. x | w R v } = { w e. x | w R y } ) )
43 breq2 
 |-  ( u = { w e. x | w R v } -> ( { w e. x | w R y } [C.] u <-> { w e. x | w R y } [C.] { w e. x | w R v } ) )
44 41 42 43 3orbi123d 
 |-  ( u = { w e. x | w R v } -> ( ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) <-> ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) ) )
45 44 ralbidv 
 |-  ( u = { w e. x | w R v } -> ( A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) <-> A. y e. x ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) ) )
46 12 45 ralrnmptw 
 |-  ( A. v e. x { w e. x | w R v } e. _V -> ( A. u e. ran ( v e. x |-> { w e. x | w R v } ) A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) <-> A. v e. x A. y e. x ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) ) )
47 11 46 ax-mp 
 |-  ( A. u e. ran ( v e. x |-> { w e. x | w R v } ) A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) <-> A. v e. x A. y e. x ( { w e. x | w R v } [C.] { w e. x | w R y } \/ { w e. x | w R v } = { w e. x | w R y } \/ { w e. x | w R y } [C.] { w e. x | w R v } ) )
48 40 47 sylibr 
 |-  ( R Or x -> A. u e. ran ( v e. x |-> { w e. x | w R v } ) A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) )
49 48 r19.21bi 
 |-  ( ( R Or x /\ u e. ran ( v e. x |-> { w e. x | w R v } ) ) -> A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) )
50 9 rabex 
 |-  { w e. x | w R y } e. _V
51 50 rgenw 
 |-  A. y e. x { w e. x | w R y } e. _V
52 34 cbvmptv 
 |-  ( v e. x |-> { w e. x | w R v } ) = ( y e. x |-> { w e. x | w R y } )
53 breq2 
 |-  ( z = { w e. x | w R y } -> ( u [C.] z <-> u [C.] { w e. x | w R y } ) )
54 eqeq2 
 |-  ( z = { w e. x | w R y } -> ( u = z <-> u = { w e. x | w R y } ) )
55 breq1 
 |-  ( z = { w e. x | w R y } -> ( z [C.] u <-> { w e. x | w R y } [C.] u ) )
56 53 54 55 3orbi123d 
 |-  ( z = { w e. x | w R y } -> ( ( u [C.] z \/ u = z \/ z [C.] u ) <-> ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) ) )
57 52 56 ralrnmptw 
 |-  ( A. y e. x { w e. x | w R y } e. _V -> ( A. z e. ran ( v e. x |-> { w e. x | w R v } ) ( u [C.] z \/ u = z \/ z [C.] u ) <-> A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) ) )
58 51 57 ax-mp 
 |-  ( A. z e. ran ( v e. x |-> { w e. x | w R v } ) ( u [C.] z \/ u = z \/ z [C.] u ) <-> A. y e. x ( u [C.] { w e. x | w R y } \/ u = { w e. x | w R y } \/ { w e. x | w R y } [C.] u ) )
59 49 58 sylibr 
 |-  ( ( R Or x /\ u e. ran ( v e. x |-> { w e. x | w R v } ) ) -> A. z e. ran ( v e. x |-> { w e. x | w R v } ) ( u [C.] z \/ u = z \/ z [C.] u ) )
60 59 r19.21bi 
 |-  ( ( ( R Or x /\ u e. ran ( v e. x |-> { w e. x | w R v } ) ) /\ z e. ran ( v e. x |-> { w e. x | w R v } ) ) -> ( u [C.] z \/ u = z \/ z [C.] u ) )
61 60 anasss 
 |-  ( ( R Or x /\ ( u e. ran ( v e. x |-> { w e. x | w R v } ) /\ z e. ran ( v e. x |-> { w e. x | w R v } ) ) ) -> ( u [C.] z \/ u = z \/ z [C.] u ) )
62 30 61 issod 
 |-  ( R Or x -> [C.] Or ran ( v e. x |-> { w e. x | w R v } ) )
63 28 62 syl 
 |-  ( ( R Or A /\ x C_ A ) -> [C.] Or ran ( v e. x |-> { w e. x | w R v } ) )
64 63 adantll 
 |-  ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) -> [C.] Or ran ( v e. x |-> { w e. x | w R v } ) )
65 64 adantr 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> [C.] Or ran ( v e. x |-> { w e. x | w R v } ) )
66 fin2i2 
 |-  ( ( ( A e. Fin2 /\ ran ( v e. x |-> { w e. x | w R v } ) C_ ~P A ) /\ ( ran ( v e. x |-> { w e. x | w R v } ) =/= (/) /\ [C.] Or ran ( v e. x |-> { w e. x | w R v } ) ) ) -> |^| ran ( v e. x |-> { w e. x | w R v } ) e. ran ( v e. x |-> { w e. x | w R v } ) )
67 1 20 26 65 66 syl22anc 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> |^| ran ( v e. x |-> { w e. x | w R v } ) e. ran ( v e. x |-> { w e. x | w R v } ) )
68 52 50 elrnmpti 
 |-  ( |^| ran ( v e. x |-> { w e. x | w R v } ) e. ran ( v e. x |-> { w e. x | w R v } ) <-> E. y e. x |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } )
69 67 68 sylib 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> E. y e. x |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } )
70 ssel2 
 |-  ( ( x C_ A /\ z e. x ) -> z e. A )
71 sonr 
 |-  ( ( R Or A /\ z e. A ) -> -. z R z )
72 70 71 sylan2 
 |-  ( ( R Or A /\ ( x C_ A /\ z e. x ) ) -> -. z R z )
73 72 anassrs 
 |-  ( ( ( R Or A /\ x C_ A ) /\ z e. x ) -> -. z R z )
74 73 adantlr 
 |-  ( ( ( ( R Or A /\ x C_ A ) /\ y e. x ) /\ z e. x ) -> -. z R z )
75 74 adantr 
 |-  ( ( ( ( ( R Or A /\ x C_ A ) /\ y e. x ) /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> -. z R z )
76 breq1 
 |-  ( w = z -> ( w R y <-> z R y ) )
77 76 elrab 
 |-  ( z e. { w e. x | w R y } <-> ( z e. x /\ z R y ) )
78 77 simplbi2 
 |-  ( z e. x -> ( z R y -> z e. { w e. x | w R y } ) )
79 78 ad2antlr 
 |-  ( ( ( y e. x /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> ( z R y -> z e. { w e. x | w R y } ) )
80 vex 
 |-  z e. _V
81 80 elint2 
 |-  ( z e. |^| ran ( v e. x |-> { w e. x | w R v } ) <-> A. y e. ran ( v e. x |-> { w e. x | w R v } ) z e. y )
82 eleq2 
 |-  ( y = { w e. x | w R v } -> ( z e. y <-> z e. { w e. x | w R v } ) )
83 12 82 ralrnmptw 
 |-  ( A. v e. x { w e. x | w R v } e. _V -> ( A. y e. ran ( v e. x |-> { w e. x | w R v } ) z e. y <-> A. v e. x z e. { w e. x | w R v } ) )
84 11 83 ax-mp 
 |-  ( A. y e. ran ( v e. x |-> { w e. x | w R v } ) z e. y <-> A. v e. x z e. { w e. x | w R v } )
85 81 84 bitri 
 |-  ( z e. |^| ran ( v e. x |-> { w e. x | w R v } ) <-> A. v e. x z e. { w e. x | w R v } )
86 breq2 
 |-  ( v = z -> ( w R v <-> w R z ) )
87 86 rabbidv 
 |-  ( v = z -> { w e. x | w R v } = { w e. x | w R z } )
88 87 eleq2d 
 |-  ( v = z -> ( z e. { w e. x | w R v } <-> z e. { w e. x | w R z } ) )
89 88 rspcv 
 |-  ( z e. x -> ( A. v e. x z e. { w e. x | w R v } -> z e. { w e. x | w R z } ) )
90 breq1 
 |-  ( w = z -> ( w R z <-> z R z ) )
91 90 elrab 
 |-  ( z e. { w e. x | w R z } <-> ( z e. x /\ z R z ) )
92 91 simprbi 
 |-  ( z e. { w e. x | w R z } -> z R z )
93 89 92 syl6 
 |-  ( z e. x -> ( A. v e. x z e. { w e. x | w R v } -> z R z ) )
94 93 adantl 
 |-  ( ( y e. x /\ z e. x ) -> ( A. v e. x z e. { w e. x | w R v } -> z R z ) )
95 85 94 syl5bi 
 |-  ( ( y e. x /\ z e. x ) -> ( z e. |^| ran ( v e. x |-> { w e. x | w R v } ) -> z R z ) )
96 eleq2 
 |-  ( |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> ( z e. |^| ran ( v e. x |-> { w e. x | w R v } ) <-> z e. { w e. x | w R y } ) )
97 96 imbi1d 
 |-  ( |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> ( ( z e. |^| ran ( v e. x |-> { w e. x | w R v } ) -> z R z ) <-> ( z e. { w e. x | w R y } -> z R z ) ) )
98 95 97 syl5ibcom 
 |-  ( ( y e. x /\ z e. x ) -> ( |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> ( z e. { w e. x | w R y } -> z R z ) ) )
99 98 imp 
 |-  ( ( ( y e. x /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> ( z e. { w e. x | w R y } -> z R z ) )
100 79 99 syld 
 |-  ( ( ( y e. x /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> ( z R y -> z R z ) )
101 100 adantlll 
 |-  ( ( ( ( ( R Or A /\ x C_ A ) /\ y e. x ) /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> ( z R y -> z R z ) )
102 75 101 mtod 
 |-  ( ( ( ( ( R Or A /\ x C_ A ) /\ y e. x ) /\ z e. x ) /\ |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } ) -> -. z R y )
103 102 ex 
 |-  ( ( ( ( R Or A /\ x C_ A ) /\ y e. x ) /\ z e. x ) -> ( |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> -. z R y ) )
104 103 ralrimdva 
 |-  ( ( ( R Or A /\ x C_ A ) /\ y e. x ) -> ( |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> A. z e. x -. z R y ) )
105 104 reximdva 
 |-  ( ( R Or A /\ x C_ A ) -> ( E. y e. x |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> E. y e. x A. z e. x -. z R y ) )
106 105 adantll 
 |-  ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) -> ( E. y e. x |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> E. y e. x A. z e. x -. z R y ) )
107 106 adantr 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> ( E. y e. x |^| ran ( v e. x |-> { w e. x | w R v } ) = { w e. x | w R y } -> E. y e. x A. z e. x -. z R y ) )
108 69 107 mpd 
 |-  ( ( ( ( A e. Fin2 /\ R Or A ) /\ x C_ A ) /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y )
109 108 expl 
 |-  ( ( A e. Fin2 /\ R Or A ) -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
110 109 alrimiv 
 |-  ( ( A e. Fin2 /\ R Or A ) -> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
111 df-fr 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
112 110 111 sylibr 
 |-  ( ( A e. Fin2 /\ R Or A ) -> R Fr A )
113 simpr 
 |-  ( ( A e. Fin2 /\ R Or A ) -> R Or A )
114 df-we 
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )
115 112 113 114 sylanbrc 
 |-  ( ( A e. Fin2 /\ R Or A ) -> R We A )
116 weinxp 
 |-  ( R We A <-> ( R i^i ( A X. A ) ) We A )
117 115 116 sylib 
 |-  ( ( A e. Fin2 /\ R Or A ) -> ( R i^i ( A X. A ) ) We A )
118 sqxpexg 
 |-  ( A e. Fin2 -> ( A X. A ) e. _V )
119 incom 
 |-  ( R i^i ( A X. A ) ) = ( ( A X. A ) i^i R )
120 inex1g 
 |-  ( ( A X. A ) e. _V -> ( ( A X. A ) i^i R ) e. _V )
121 119 120 eqeltrid 
 |-  ( ( A X. A ) e. _V -> ( R i^i ( A X. A ) ) e. _V )
122 weeq1 
 |-  ( z = ( R i^i ( A X. A ) ) -> ( z We A <-> ( R i^i ( A X. A ) ) We A ) )
123 122 spcegv 
 |-  ( ( R i^i ( A X. A ) ) e. _V -> ( ( R i^i ( A X. A ) ) We A -> E. z z We A ) )
124 118 121 123 3syl 
 |-  ( A e. Fin2 -> ( ( R i^i ( A X. A ) ) We A -> E. z z We A ) )
125 124 imp 
 |-  ( ( A e. Fin2 /\ ( R i^i ( A X. A ) ) We A ) -> E. z z We A )
126 117 125 syldan 
 |-  ( ( A e. Fin2 /\ R Or A ) -> E. z z We A )
127 ween 
 |-  ( A e. dom card <-> E. z z We A )
128 126 127 sylibr 
 |-  ( ( A e. Fin2 /\ R Or A ) -> A e. dom card )
129 fin23 
 |-  ( A e. Fin2 -> A e. Fin3 )
130 fin34 
 |-  ( A e. Fin3 -> A e. Fin4 )
131 fin45 
 |-  ( A e. Fin4 -> A e. Fin5 )
132 129 130 131 3syl 
 |-  ( A e. Fin2 -> A e. Fin5 )
133 fin56 
 |-  ( A e. Fin5 -> A e. Fin6 )
134 fin67 
 |-  ( A e. Fin6 -> A e. Fin7 )
135 132 133 134 3syl 
 |-  ( A e. Fin2 -> A e. Fin7 )
136 fin71num 
 |-  ( A e. dom card -> ( A e. Fin7 <-> A e. Fin ) )
137 136 biimpac 
 |-  ( ( A e. Fin7 /\ A e. dom card ) -> A e. Fin )
138 135 137 sylan 
 |-  ( ( A e. Fin2 /\ A e. dom card ) -> A e. Fin )
139 128 138 syldan 
 |-  ( ( A e. Fin2 /\ R Or A ) -> A e. Fin )