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 ⊢ 𝐴 ∈ V
domunsncan.b ⊢ 𝐵 ∈ V
Assertion domunsncan ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) → ( ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )

Proof

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