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 difexg ⊢ ( ( { 𝐵 } ∪ 𝑌 ) ∈ V → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ∈ V )
27 25 26 syl ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ∈ V )
28 f1f ⊢ ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → 𝑓 : ( { 𝐴 } ∪ 𝑋 ) ⟶ ( { 𝐵 } ∪ 𝑌 ) )
29 fimass ⊢ ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) ⟶ ( { 𝐵 } ∪ 𝑌 ) → ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ⊆ ( { 𝐵 } ∪ 𝑌 ) )
30 28 29 syl ⊢ ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ⊆ ( { 𝐵 } ∪ 𝑌 ) )
31 30 ad2antll ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ⊆ ( { 𝐵 } ∪ 𝑌 ) )
32 31 ssdifd ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ⊆ ( ( { 𝐵 } ∪ 𝑌 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
33 f1fn ⊢ ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → 𝑓 Fn ( { 𝐴 } ∪ 𝑋 ) )
34 33 ad2antll ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → 𝑓 Fn ( { 𝐴 } ∪ 𝑋 ) )
35 1 snid ⊢ 𝐴 ∈ { 𝐴 }
36 elun1 ⊢ ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ ( { 𝐴 } ∪ 𝑋 ) )
37 35 36 ax-mp ⊢ 𝐴 ∈ ( { 𝐴 } ∪ 𝑋 )
38 fnsnfv ⊢ ( ( 𝑓 Fn ( { 𝐴 } ∪ 𝑋 ) ∧ 𝐴 ∈ ( { 𝐴 } ∪ 𝑋 ) ) → { ( 𝑓 ‘ 𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
39 34 37 38 sylancl ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → { ( 𝑓 ‘ 𝐴 ) } = ( 𝑓 “ { 𝐴 } ) )
40 39 difeq2d ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) = ( ( { 𝐵 } ∪ 𝑌 ) ∖ ( 𝑓 “ { 𝐴 } ) ) )
41 32 40 sseqtrrd ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ⊆ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
42 ssdomg ⊢ ( ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ∈ V → ( ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ⊆ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ) )
43 27 41 42 sylc ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) )
44 ffvelrn ⊢ ( ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) ⟶ ( { 𝐵 } ∪ 𝑌 ) ∧ 𝐴 ∈ ( { 𝐴 } ∪ 𝑋 ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ( { 𝐵 } ∪ 𝑌 ) )
45 28 37 44 sylancl ⊢ ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → ( 𝑓 ‘ 𝐴 ) ∈ ( { 𝐵 } ∪ 𝑌 ) )
46 45 ad2antll ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( 𝑓 ‘ 𝐴 ) ∈ ( { 𝐵 } ∪ 𝑌 ) )
47 2 snid ⊢ 𝐵 ∈ { 𝐵 }
48 elun1 ⊢ ( 𝐵 ∈ { 𝐵 } → 𝐵 ∈ ( { 𝐵 } ∪ 𝑌 ) )
49 47 48 mp1i ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → 𝐵 ∈ ( { 𝐵 } ∪ 𝑌 ) )
50 difsnen ⊢ ( ( ( { 𝐵 } ∪ 𝑌 ) ∈ V ∧ ( 𝑓 ‘ 𝐴 ) ∈ ( { 𝐵 } ∪ 𝑌 ) ∧ 𝐵 ∈ ( { 𝐵 } ∪ 𝑌 ) ) → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
51 25 46 49 50 syl3anc ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
52 domentr ⊢ ( ( ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ∧ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { ( 𝑓 ‘ 𝐴 ) } ) ≈ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
53 43 51 52 syl2anc ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( 𝑓 “ ( { 𝐴 } ∪ 𝑋 ) ) ∖ ( 𝑓 “ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
54 21 53 eqbrtrd ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( 𝑓 “ ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
55 endomtr ⊢ ( ( ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ≈ ( 𝑓 “ ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ) ∧ ( 𝑓 “ ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) ) → ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
56 17 54 55 syl2anc ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) ≼ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) )
57 uncom ⊢ ( { 𝐴 } ∪ 𝑋 ) = ( 𝑋 ∪ { 𝐴 } )
58 57 difeq1i ⊢ ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) = ( ( 𝑋 ∪ { 𝐴 } ) ∖ { 𝐴 } )
59 difun2 ⊢ ( ( 𝑋 ∪ { 𝐴 } ) ∖ { 𝐴 } ) = ( 𝑋 ∖ { 𝐴 } )
60 58 59 eqtri ⊢ ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) = ( 𝑋 ∖ { 𝐴 } )
61 difsn ⊢ ( ¬ 𝐴 ∈ 𝑋 → ( 𝑋 ∖ { 𝐴 } ) = 𝑋 )
62 60 61 syl5eq ⊢ ( ¬ 𝐴 ∈ 𝑋 → ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) = 𝑋 )
63 62 ad2antrr ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐴 } ∪ 𝑋 ) ∖ { 𝐴 } ) = 𝑋 )
64 uncom ⊢ ( { 𝐵 } ∪ 𝑌 ) = ( 𝑌 ∪ { 𝐵 } )
65 64 difeq1i ⊢ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) = ( ( 𝑌 ∪ { 𝐵 } ) ∖ { 𝐵 } )
66 difun2 ⊢ ( ( 𝑌 ∪ { 𝐵 } ) ∖ { 𝐵 } ) = ( 𝑌 ∖ { 𝐵 } )
67 65 66 eqtri ⊢ ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) = ( 𝑌 ∖ { 𝐵 } )
68 difsn ⊢ ( ¬ 𝐵 ∈ 𝑌 → ( 𝑌 ∖ { 𝐵 } ) = 𝑌 )
69 67 68 syl5eq ⊢ ( ¬ 𝐵 ∈ 𝑌 → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) = 𝑌 )
70 69 ad2antlr ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → ( ( { 𝐵 } ∪ 𝑌 ) ∖ { 𝐵 } ) = 𝑌 )
71 56 63 70 3brtr3d ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( 𝑌 ∈ V ∧ 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) ) ) → 𝑋 ≼ 𝑌 )
72 71 expr ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑌 ∈ V ) → ( 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → 𝑋 ≼ 𝑌 ) )
73 72 exlimdv ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑌 ∈ V ) → ( ∃ 𝑓 𝑓 : ( { 𝐴 } ∪ 𝑋 ) –1-1→ ( { 𝐵 } ∪ 𝑌 ) → 𝑋 ≼ 𝑌 ) )
74 9 73 syl5 ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑌 ∈ V ) → ( ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) → 𝑋 ≼ 𝑌 ) )
75 74 impancom ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) ) → ( 𝑌 ∈ V → 𝑋 ≼ 𝑌 ) )
76 8 75 mpd ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) ) → 𝑋 ≼ 𝑌 )
77 en2sn ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝐴 } ≈ { 𝐵 } )
78 1 2 77 mp2an ⊢ { 𝐴 } ≈ { 𝐵 }
79 endom ⊢ ( { 𝐴 } ≈ { 𝐵 } → { 𝐴 } ≼ { 𝐵 } )
80 78 79 mp1i ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑋 ≼ 𝑌 ) → { 𝐴 } ≼ { 𝐵 } )
81 simpr ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑋 ≼ 𝑌 ) → 𝑋 ≼ 𝑌 )
82 incom ⊢ ( { 𝐵 } ∩ 𝑌 ) = ( 𝑌 ∩ { 𝐵 } )
83 disjsn ⊢ ( ( 𝑌 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝑌 )
84 83 biimpri ⊢ ( ¬ 𝐵 ∈ 𝑌 → ( 𝑌 ∩ { 𝐵 } ) = ∅ )
85 82 84 syl5eq ⊢ ( ¬ 𝐵 ∈ 𝑌 → ( { 𝐵 } ∩ 𝑌 ) = ∅ )
86 85 ad2antlr ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑋 ≼ 𝑌 ) → ( { 𝐵 } ∩ 𝑌 ) = ∅ )
87 undom ⊢ ( ( ( { 𝐴 } ≼ { 𝐵 } ∧ 𝑋 ≼ 𝑌 ) ∧ ( { 𝐵 } ∩ 𝑌 ) = ∅ ) → ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) )
88 80 81 86 87 syl21anc ⊢ ( ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) ∧ 𝑋 ≼ 𝑌 ) → ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) )
89 76 88 impbida ⊢ ( ( ¬ 𝐴 ∈ 𝑋 ∧ ¬ 𝐵 ∈ 𝑌 ) → ( ( { 𝐴 } ∪ 𝑋 ) ≼ ( { 𝐵 } ∪ 𝑌 ) ↔ 𝑋 ≼ 𝑌 ) )