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

Metamath Proof Explorer

Theorem domunfican

Description: A finite set union cancellation law for dominance. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

Ref Expression
Assertion domunfican 
|- ( ( ( A e. Fin /\ B ~~ A ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( B ~~ A -> A ~~ B )
2 bren 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )
3 1 2 sylib 
 |-  ( B ~~ A -> E. f f : A -1-1-onto-> B )
4 ssid 
 |-  A C_ A
5 sseq1 
 |-  ( a = (/) -> ( a C_ A <-> (/) C_ A ) )
6 5 anbi1d 
 |-  ( a = (/) -> ( ( a C_ A /\ f : A -1-1-onto-> B ) <-> ( (/) C_ A /\ f : A -1-1-onto-> B ) ) )
7 6 anbi1d 
 |-  ( a = (/) -> ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) <-> ( ( (/) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) )
8 uneq1 
 |-  ( a = (/) -> ( a u. X ) = ( (/) u. X ) )
9 imaeq2 
 |-  ( a = (/) -> ( f " a ) = ( f " (/) ) )
10 9 uneq1d 
 |-  ( a = (/) -> ( ( f " a ) u. Y ) = ( ( f " (/) ) u. Y ) )
11 8 10 breq12d 
 |-  ( a = (/) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> ( (/) u. X ) ~<_ ( ( f " (/) ) u. Y ) ) )
12 11 bibi1d 
 |-  ( a = (/) -> ( ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) <-> ( ( (/) u. X ) ~<_ ( ( f " (/) ) u. Y ) <-> X ~<_ Y ) ) )
13 7 12 imbi12d 
 |-  ( a = (/) -> ( ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) ) <-> ( ( ( (/) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( (/) u. X ) ~<_ ( ( f " (/) ) u. Y ) <-> X ~<_ Y ) ) ) )
14 sseq1 
 |-  ( a = b -> ( a C_ A <-> b C_ A ) )
15 14 anbi1d 
 |-  ( a = b -> ( ( a C_ A /\ f : A -1-1-onto-> B ) <-> ( b C_ A /\ f : A -1-1-onto-> B ) ) )
16 15 anbi1d 
 |-  ( a = b -> ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) <-> ( ( b C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) )
17 uneq1 
 |-  ( a = b -> ( a u. X ) = ( b u. X ) )
18 imaeq2 
 |-  ( a = b -> ( f " a ) = ( f " b ) )
19 18 uneq1d 
 |-  ( a = b -> ( ( f " a ) u. Y ) = ( ( f " b ) u. Y ) )
20 17 19 breq12d 
 |-  ( a = b -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) )
21 20 bibi1d 
 |-  ( a = b -> ( ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) <-> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) )
22 16 21 imbi12d 
 |-  ( a = b -> ( ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) ) <-> ( ( ( b C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) ) )
23 sseq1 
 |-  ( a = ( b u. { c } ) -> ( a C_ A <-> ( b u. { c } ) C_ A ) )
24 23 anbi1d 
 |-  ( a = ( b u. { c } ) -> ( ( a C_ A /\ f : A -1-1-onto-> B ) <-> ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) ) )
25 24 anbi1d 
 |-  ( a = ( b u. { c } ) -> ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) <-> ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) )
26 uneq1 
 |-  ( a = ( b u. { c } ) -> ( a u. X ) = ( ( b u. { c } ) u. X ) )
27 imaeq2 
 |-  ( a = ( b u. { c } ) -> ( f " a ) = ( f " ( b u. { c } ) ) )
28 27 uneq1d 
 |-  ( a = ( b u. { c } ) -> ( ( f " a ) u. Y ) = ( ( f " ( b u. { c } ) ) u. Y ) )
29 26 28 breq12d 
 |-  ( a = ( b u. { c } ) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) ) )
30 29 bibi1d 
 |-  ( a = ( b u. { c } ) -> ( ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) <-> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) )
31 25 30 imbi12d 
 |-  ( a = ( b u. { c } ) -> ( ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) ) <-> ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) ) )
32 sseq1 
 |-  ( a = A -> ( a C_ A <-> A C_ A ) )
33 32 anbi1d 
 |-  ( a = A -> ( ( a C_ A /\ f : A -1-1-onto-> B ) <-> ( A C_ A /\ f : A -1-1-onto-> B ) ) )
34 33 anbi1d 
 |-  ( a = A -> ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) <-> ( ( A C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) )
35 uneq1 
 |-  ( a = A -> ( a u. X ) = ( A u. X ) )
36 imaeq2 
 |-  ( a = A -> ( f " a ) = ( f " A ) )
37 36 uneq1d 
 |-  ( a = A -> ( ( f " a ) u. Y ) = ( ( f " A ) u. Y ) )
38 35 37 breq12d 
 |-  ( a = A -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> ( A u. X ) ~<_ ( ( f " A ) u. Y ) ) )
39 38 bibi1d 
 |-  ( a = A -> ( ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) <-> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) ) )
40 34 39 imbi12d 
 |-  ( a = A -> ( ( ( ( a C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( a u. X ) ~<_ ( ( f " a ) u. Y ) <-> X ~<_ Y ) ) <-> ( ( ( A C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) ) ) )
41 uncom 
 |-  ( (/) u. X ) = ( X u. (/) )
42 un0 
 |-  ( X u. (/) ) = X
43 41 42 eqtri 
 |-  ( (/) u. X ) = X
44 ima0 
 |-  ( f " (/) ) = (/)
45 44 uneq1i 
 |-  ( ( f " (/) ) u. Y ) = ( (/) u. Y )
46 uncom 
 |-  ( (/) u. Y ) = ( Y u. (/) )
47 un0 
 |-  ( Y u. (/) ) = Y
48 46 47 eqtri 
 |-  ( (/) u. Y ) = Y
49 45 48 eqtri 
 |-  ( ( f " (/) ) u. Y ) = Y
50 43 49 breq12i 
 |-  ( ( (/) u. X ) ~<_ ( ( f " (/) ) u. Y ) <-> X ~<_ Y )
51 50 a1i 
 |-  ( ( ( (/) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( (/) u. X ) ~<_ ( ( f " (/) ) u. Y ) <-> X ~<_ Y ) )
52 ssun1 
 |-  b C_ ( b u. { c } )
53 sstr2 
 |-  ( b C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ A -> b C_ A ) )
54 52 53 ax-mp 
 |-  ( ( b u. { c } ) C_ A -> b C_ A )
55 54 anim1i 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> ( b C_ A /\ f : A -1-1-onto-> B ) )
56 55 anim1i 
 |-  ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) )
57 56 imim1i 
 |-  ( ( ( ( b C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) -> ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) )
58 uncom 
 |-  ( b u. { c } ) = ( { c } u. b )
59 58 uneq1i 
 |-  ( ( b u. { c } ) u. X ) = ( ( { c } u. b ) u. X )
60 unass 
 |-  ( ( { c } u. b ) u. X ) = ( { c } u. ( b u. X ) )
61 59 60 eqtri 
 |-  ( ( b u. { c } ) u. X ) = ( { c } u. ( b u. X ) )
62 61 a1i 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( b u. { c } ) u. X ) = ( { c } u. ( b u. X ) ) )
63 imaundi 
 |-  ( f " ( b u. { c } ) ) = ( ( f " b ) u. ( f " { c } ) )
64 simprlr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> f : A -1-1-onto-> B )
65 f1ofn 
 |-  ( f : A -1-1-onto-> B -> f Fn A )
66 64 65 syl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> f Fn A )
67 ssun2 
 |-  { c } C_ ( b u. { c } )
68 sstr2 
 |-  ( { c } C_ ( b u. { c } ) -> ( ( b u. { c } ) C_ A -> { c } C_ A ) )
69 67 68 ax-mp 
 |-  ( ( b u. { c } ) C_ A -> { c } C_ A )
70 vex 
 |-  c e. _V
71 70 snss 
 |-  ( c e. A <-> { c } C_ A )
72 69 71 sylibr 
 |-  ( ( b u. { c } ) C_ A -> c e. A )
73 72 adantr 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> c e. A )
74 73 ad2antrl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> c e. A )
75 fnsnfv 
 |-  ( ( f Fn A /\ c e. A ) -> { ( f ` c ) } = ( f " { c } ) )
76 66 74 75 syl2anc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> { ( f ` c ) } = ( f " { c } ) )
77 76 eqcomd 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( f " { c } ) = { ( f ` c ) } )
78 77 uneq2d 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( f " b ) u. ( f " { c } ) ) = ( ( f " b ) u. { ( f ` c ) } ) )
79 63 78 eqtrid 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( f " ( b u. { c } ) ) = ( ( f " b ) u. { ( f ` c ) } ) )
80 79 uneq1d 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( f " ( b u. { c } ) ) u. Y ) = ( ( ( f " b ) u. { ( f ` c ) } ) u. Y ) )
81 uncom 
 |-  ( ( f " b ) u. { ( f ` c ) } ) = ( { ( f ` c ) } u. ( f " b ) )
82 81 uneq1i 
 |-  ( ( ( f " b ) u. { ( f ` c ) } ) u. Y ) = ( ( { ( f ` c ) } u. ( f " b ) ) u. Y )
83 unass 
 |-  ( ( { ( f ` c ) } u. ( f " b ) ) u. Y ) = ( { ( f ` c ) } u. ( ( f " b ) u. Y ) )
84 82 83 eqtri 
 |-  ( ( ( f " b ) u. { ( f ` c ) } ) u. Y ) = ( { ( f ` c ) } u. ( ( f " b ) u. Y ) )
85 80 84 eqtrdi 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( f " ( b u. { c } ) ) u. Y ) = ( { ( f ` c ) } u. ( ( f " b ) u. Y ) ) )
86 62 85 breq12d 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> ( { c } u. ( b u. X ) ) ~<_ ( { ( f ` c ) } u. ( ( f " b ) u. Y ) ) ) )
87 simplr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. c e. b )
88 incom 
 |-  ( X i^i A ) = ( A i^i X )
89 simprrl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( A i^i X ) = (/) )
90 88 89 eqtrid 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( X i^i A ) = (/) )
91 minel 
 |-  ( ( c e. A /\ ( X i^i A ) = (/) ) -> -. c e. X )
92 74 90 91 syl2anc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. c e. X )
93 ioran 
 |-  ( -. ( c e. b \/ c e. X ) <-> ( -. c e. b /\ -. c e. X ) )
94 elun 
 |-  ( c e. ( b u. X ) <-> ( c e. b \/ c e. X ) )
95 93 94 xchnxbir 
 |-  ( -. c e. ( b u. X ) <-> ( -. c e. b /\ -. c e. X ) )
96 87 92 95 sylanbrc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. c e. ( b u. X ) )
97 simplr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) ) -> -. c e. b )
98 f1of1 
 |-  ( f : A -1-1-onto-> B -> f : A -1-1-> B )
99 98 adantl 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> f : A -1-1-> B )
100 54 adantr 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> b C_ A )
101 f1elima 
 |-  ( ( f : A -1-1-> B /\ c e. A /\ b C_ A ) -> ( ( f ` c ) e. ( f " b ) <-> c e. b ) )
102 99 73 100 101 syl3anc 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> ( ( f ` c ) e. ( f " b ) <-> c e. b ) )
103 102 biimpd 
 |-  ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) -> ( ( f ` c ) e. ( f " b ) -> c e. b ) )
104 103 adantl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) ) -> ( ( f ` c ) e. ( f " b ) -> c e. b ) )
105 97 104 mtod 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) ) -> -. ( f ` c ) e. ( f " b ) )
106 105 adantrr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. ( f ` c ) e. ( f " b ) )
107 f1of 
 |-  ( f : A -1-1-onto-> B -> f : A --> B )
108 64 107 syl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> f : A --> B )
109 108 74 ffvelcdmd 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( f ` c ) e. B )
110 incom 
 |-  ( Y i^i B ) = ( B i^i Y )
111 simprrr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( B i^i Y ) = (/) )
112 110 111 eqtrid 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( Y i^i B ) = (/) )
113 minel 
 |-  ( ( ( f ` c ) e. B /\ ( Y i^i B ) = (/) ) -> -. ( f ` c ) e. Y )
114 109 112 113 syl2anc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. ( f ` c ) e. Y )
115 ioran 
 |-  ( -. ( ( f ` c ) e. ( f " b ) \/ ( f ` c ) e. Y ) <-> ( -. ( f ` c ) e. ( f " b ) /\ -. ( f ` c ) e. Y ) )
116 elun 
 |-  ( ( f ` c ) e. ( ( f " b ) u. Y ) <-> ( ( f ` c ) e. ( f " b ) \/ ( f ` c ) e. Y ) )
117 115 116 xchnxbir 
 |-  ( -. ( f ` c ) e. ( ( f " b ) u. Y ) <-> ( -. ( f ` c ) e. ( f " b ) /\ -. ( f ` c ) e. Y ) )
118 106 114 117 sylanbrc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> -. ( f ` c ) e. ( ( f " b ) u. Y ) )
119 fvex 
 |-  ( f ` c ) e. _V
120 70 119 domunsncan 
 |-  ( ( -. c e. ( b u. X ) /\ -. ( f ` c ) e. ( ( f " b ) u. Y ) ) -> ( ( { c } u. ( b u. X ) ) ~<_ ( { ( f ` c ) } u. ( ( f " b ) u. Y ) ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) )
121 96 118 120 syl2anc 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( { c } u. ( b u. X ) ) ~<_ ( { ( f ` c ) } u. ( ( f " b ) u. Y ) ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) )
122 86 121 bitrd 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) )
123 bitr 
 |-  ( ( ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) /\ ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) )
124 123 ex 
 |-  ( ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> ( b u. X ) ~<_ ( ( f " b ) u. Y ) ) -> ( ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) )
125 122 124 syl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) ) -> ( ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) )
126 125 ex 
 |-  ( ( b e. Fin /\ -. c e. b ) -> ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) ) )
127 126 a2d 
 |-  ( ( b e. Fin /\ -. c e. b ) -> ( ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) -> ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) ) )
128 57 127 syl5 
 |-  ( ( b e. Fin /\ -. c e. b ) -> ( ( ( ( b C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( b u. X ) ~<_ ( ( f " b ) u. Y ) <-> X ~<_ Y ) ) -> ( ( ( ( b u. { c } ) C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( ( b u. { c } ) u. X ) ~<_ ( ( f " ( b u. { c } ) ) u. Y ) <-> X ~<_ Y ) ) ) )
129 13 22 31 40 51 128 findcard2s 
 |-  ( A e. Fin -> ( ( ( A C_ A /\ f : A -1-1-onto-> B ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) ) )
130 129 expd 
 |-  ( A e. Fin -> ( ( A C_ A /\ f : A -1-1-onto-> B ) -> ( ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) ) ) )
131 4 130 mpani 
 |-  ( A e. Fin -> ( f : A -1-1-onto-> B -> ( ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) ) ) )
132 131 3imp 
 |-  ( ( A e. Fin /\ f : A -1-1-onto-> B /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) )
133 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
134 foima 
 |-  ( f : A -onto-> B -> ( f " A ) = B )
135 133 134 syl 
 |-  ( f : A -1-1-onto-> B -> ( f " A ) = B )
136 135 uneq1d 
 |-  ( f : A -1-1-onto-> B -> ( ( f " A ) u. Y ) = ( B u. Y ) )
137 136 breq2d 
 |-  ( f : A -1-1-onto-> B -> ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> ( A u. X ) ~<_ ( B u. Y ) ) )
138 137 bibi1d 
 |-  ( f : A -1-1-onto-> B -> ( ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) <-> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) ) )
139 138 3ad2ant2 
 |-  ( ( A e. Fin /\ f : A -1-1-onto-> B /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( ( A u. X ) ~<_ ( ( f " A ) u. Y ) <-> X ~<_ Y ) <-> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) ) )
140 132 139 mpbid 
 |-  ( ( A e. Fin /\ f : A -1-1-onto-> B /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) )
141 140 3exp 
 |-  ( A e. Fin -> ( f : A -1-1-onto-> B -> ( ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) ) ) )
142 141 exlimdv 
 |-  ( A e. Fin -> ( E. f f : A -1-1-onto-> B -> ( ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) ) ) )
143 3 142 syl5 
 |-  ( A e. Fin -> ( B ~~ A -> ( ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) ) ) )
144 143 imp31 
 |-  ( ( ( A e. Fin /\ B ~~ A ) /\ ( ( A i^i X ) = (/) /\ ( B i^i Y ) = (/) ) ) -> ( ( A u. X ) ~<_ ( B u. Y ) <-> X ~<_ Y ) )