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 ffvelrnd
 |-  ( ( ( 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 ) )