Metamath Proof Explorer

Theorem domunsncan

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

Ref Expression
Hypotheses domunsncan.a ⊢A∈V
domunsncan.b ⊢B∈V
Assertion domunsncan ⊢¬A∈X∧¬B∈Y→A∪X≼B∪Y↔X≼Y

Proof

Step Hyp Ref Expression
1 domunsncan.a ⊢A∈V
2 domunsncan.b ⊢B∈V
3 ssun2 ⊢Y⊆B∪Y
4 reldom ⊢Rel⁡≼
5 4 brrelex2i ⊢A∪X≼B∪Y→B∪Y∈V
6 5 adantl ⊢¬A∈X∧¬B∈Y∧A∪X≼B∪Y→B∪Y∈V
7 ssexg ⊢Y⊆B∪Y∧B∪Y∈V→Y∈V
8 3 6 7 sylancr ⊢¬A∈X∧¬B∈Y∧A∪X≼B∪Y→Y∈V
9 brdomi ⊢A∪X≼B∪Y→∃ff:A∪X⟶1-1B∪Y
10 vex ⊢f∈V
11 10 resex ⊢f↾A∪X∖A∈V
12 simprr ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→f:A∪X⟶1-1B∪Y
13 difss ⊢A∪X∖A⊆A∪X
14 f1ores ⊢f:A∪X⟶1-1B∪Y∧A∪X∖A⊆A∪X→f↾A∪X∖A:A∪X∖A⟶1-1 ontofA∪X∖A
15 12 13 14 sylancl ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→f↾A∪X∖A:A∪X∖A⟶1-1 ontofA∪X∖A
16 f1oen3g ⊢f↾A∪X∖A∈V∧f↾A∪X∖A:A∪X∖A⟶1-1 ontofA∪X∖A→A∪X∖A≈fA∪X∖A
17 11 15 16 sylancr ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→A∪X∖A≈fA∪X∖A
18 df-f1 ⊢f:A∪X⟶1-1B∪Y↔f:A∪X⟶B∪Y∧Fun⁡f-1
19 imadif ⊢Fun⁡f-1→fA∪X∖A=fA∪X∖fA
20 18 19 simplbiim ⊢f:A∪X⟶1-1B∪Y→fA∪X∖A=fA∪X∖fA
21 20 ad2antll ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖A=fA∪X∖fA
22 snex ⊢B∈V
23 simprl ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→Y∈V
24 unexg ⊢B∈V∧Y∈V→B∪Y∈V
25 22 23 24 sylancr ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∪Y∈V
26 25 difexd ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∪Y∖f⁡A∈V
27 f1f ⊢f:A∪X⟶1-1B∪Y→f:A∪X⟶B∪Y
28 fimass ⊢f:A∪X⟶B∪Y→fA∪X⊆B∪Y
29 27 28 syl ⊢f:A∪X⟶1-1B∪Y→fA∪X⊆B∪Y
30 29 ad2antll ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X⊆B∪Y
31 30 ssdifd ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖fA⊆B∪Y∖fA
32 f1fn ⊢f:A∪X⟶1-1B∪Y→fFnA∪X
33 32 ad2antll ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fFnA∪X
34 1 snid ⊢A∈A
35 elun1 ⊢A∈A→A∈A∪X
36 34 35 ax-mp ⊢A∈A∪X
37 fnsnfv ⊢fFnA∪X∧A∈A∪X→f⁡A=fA
38 33 36 37 sylancl ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→f⁡A=fA
39 38 difeq2d ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∪Y∖f⁡A=B∪Y∖fA
40 31 39 sseqtrrd ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖fA⊆B∪Y∖f⁡A
41 ssdomg ⊢B∪Y∖f⁡A∈V→fA∪X∖fA⊆B∪Y∖f⁡A→fA∪X∖fA≼B∪Y∖f⁡A
42 26 40 41 sylc ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖fA≼B∪Y∖f⁡A
43 ffvelcdm ⊢f:A∪X⟶B∪Y∧A∈A∪X→f⁡A∈B∪Y
44 27 36 43 sylancl ⊢f:A∪X⟶1-1B∪Y→f⁡A∈B∪Y
45 44 ad2antll ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→f⁡A∈B∪Y
46 2 snid ⊢B∈B
47 elun1 ⊢B∈B→B∈B∪Y
48 46 47 mp1i ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∈B∪Y
49 difsnen ⊢B∪Y∈V∧f⁡A∈B∪Y∧B∈B∪Y→B∪Y∖f⁡A≈B∪Y∖B
50 25 45 48 49 syl3anc ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∪Y∖f⁡A≈B∪Y∖B
51 domentr ⊢fA∪X∖fA≼B∪Y∖f⁡A∧B∪Y∖f⁡A≈B∪Y∖B→fA∪X∖fA≼B∪Y∖B
52 42 50 51 syl2anc ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖fA≼B∪Y∖B
53 21 52 eqbrtrd ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→fA∪X∖A≼B∪Y∖B
54 endomtr ⊢A∪X∖A≈fA∪X∖A∧fA∪X∖A≼B∪Y∖B→A∪X∖A≼B∪Y∖B
55 17 53 54 syl2anc ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→A∪X∖A≼B∪Y∖B
56 uncom ⊢A∪X=X∪A
57 56 difeq1i ⊢A∪X∖A=X∪A∖A
58 difun2 ⊢X∪A∖A=X∖A
59 57 58 eqtri ⊢A∪X∖A=X∖A
60 difsn ⊢¬A∈X→X∖A=X
61 59 60 eqtrid ⊢¬A∈X→A∪X∖A=X
62 61 ad2antrr ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→A∪X∖A=X
63 uncom ⊢B∪Y=Y∪B
64 63 difeq1i ⊢B∪Y∖B=Y∪B∖B
65 difun2 ⊢Y∪B∖B=Y∖B
66 64 65 eqtri ⊢B∪Y∖B=Y∖B
67 difsn ⊢¬B∈Y→Y∖B=Y
68 66 67 eqtrid ⊢¬B∈Y→B∪Y∖B=Y
69 68 ad2antlr ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→B∪Y∖B=Y
70 55 62 69 3brtr3d ⊢¬A∈X∧¬B∈Y∧Y∈V∧f:A∪X⟶1-1B∪Y→X≼Y
71 70 expr ⊢¬A∈X∧¬B∈Y∧Y∈V→f:A∪X⟶1-1B∪Y→X≼Y
72 71 exlimdv ⊢¬A∈X∧¬B∈Y∧Y∈V→∃ff:A∪X⟶1-1B∪Y→X≼Y
73 9 72 syl5 ⊢¬A∈X∧¬B∈Y∧Y∈V→A∪X≼B∪Y→X≼Y
74 73 impancom ⊢¬A∈X∧¬B∈Y∧A∪X≼B∪Y→Y∈V→X≼Y
75 8 74 mpd ⊢¬A∈X∧¬B∈Y∧A∪X≼B∪Y→X≼Y
76 en2sn ⊢A∈V∧B∈V→A≈B
77 1 2 76 mp2an ⊢A≈B
78 endom ⊢A≈B→A≼B
79 77 78 mp1i ⊢¬A∈X∧¬B∈Y∧X≼Y→A≼B
80 simpr ⊢¬A∈X∧¬B∈Y∧X≼Y→X≼Y
81 incom ⊢B∩Y=Y∩B
82 disjsn ⊢Y∩B=∅↔¬B∈Y
83 82 biimpri ⊢¬B∈Y→Y∩B=∅
84 81 83 eqtrid ⊢¬B∈Y→B∩Y=∅
85 84 ad2antlr ⊢¬A∈X∧¬B∈Y∧X≼Y→B∩Y=∅
86 undom ⊢A≼B∧X≼Y∧B∩Y=∅→A∪X≼B∪Y
87 79 80 85 86 syl21anc ⊢¬A∈X∧¬B∈Y∧X≼Y→A∪X≼B∪Y
88 75 87 impbida ⊢¬A∈X∧¬B∈Y→A∪X≼B∪Y↔X≼Y