Metamath Proof Explorer

Theorem domdifsn

Description: Dominance over a set with one element removed. (Contributed by Stefan O'Rear, 19-Feb-2015) (Revised by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion domdifsn ( 𝐴 ≺ 𝐵 → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 relsdom ⊢ Rel ≺
3 2 brrelex2i ⊢ ( 𝐴 ≺ 𝐵 → 𝐵 ∈ V )
4 brdomg ⊢ ( 𝐵 ∈ V → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
5 3 4 syl ⊢ ( 𝐴 ≺ 𝐵 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
6 1 5 mpbid ⊢ ( 𝐴 ≺ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
7 6 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
8 f1f ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
9 8 frnd ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ran 𝑓 ⊆ 𝐵 )
10 9 adantl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ran 𝑓 ⊆ 𝐵 )
11 sdomnen ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
12 11 ad2antrr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )
13 vex ⊢ 𝑓 ∈ V
14 dff1o5 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 = 𝐵 ) )
15 14 biimpri ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 = 𝐵 ) → 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
16 f1oen3g ⊢ ( ( 𝑓 ∈ V ∧ 𝑓 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐴 ≈ 𝐵 )
17 13 15 16 sylancr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 = 𝐵 ) → 𝐴 ≈ 𝐵 )
18 17 ex ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( ran 𝑓 = 𝐵 → 𝐴 ≈ 𝐵 ) )
19 18 necon3bd ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( ¬ 𝐴 ≈ 𝐵 → ran 𝑓 ≠ 𝐵 ) )
20 19 adantl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ¬ 𝐴 ≈ 𝐵 → ran 𝑓 ≠ 𝐵 ) )
21 12 20 mpd ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ran 𝑓 ≠ 𝐵 )
22 pssdifn0 ⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ran 𝑓 ≠ 𝐵 ) → ( 𝐵 ∖ ran 𝑓 ) ≠ ∅ )
23 10 21 22 syl2anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝐵 ∖ ran 𝑓 ) ≠ ∅ )
24 n0 ⊢ ( ( 𝐵 ∖ ran 𝑓 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) )
25 23 24 sylib ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) )
26 2 brrelex1i ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ∈ V )
27 26 ad2antrr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐴 ∈ V )
28 3 ad2antrr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐵 ∈ V )
29 28 difexd ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ∈ V )
30 eldifn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → ¬ 𝑥 ∈ ran 𝑓 )
31 disjsn ⊢ ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ran 𝑓 )
32 30 31 sylibr ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → ( ran 𝑓 ∩ { 𝑥 } ) = ∅ )
33 32 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ( ran 𝑓 ∩ { 𝑥 } ) = ∅ )
34 9 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ran 𝑓 ⊆ 𝐵 )
35 reldisj ⊢ ( ran 𝑓 ⊆ 𝐵 → ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) )
36 34 35 syl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) )
37 33 36 mpbid ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) )
38 f1ssr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
39 37 38 syldan ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
40 39 adantl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
41 f1dom2g ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐵 ∖ { 𝑥 } ) ∈ V ∧ 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) )
42 27 29 40 41 syl3anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) )
43 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝑥 ∈ 𝐵 )
44 43 ad2antll ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝑥 ∈ 𝐵 )
45 simplr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐶 ∈ 𝐵 )
46 difsnen ⊢ ( ( 𝐵 ∈ V ∧ 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) )
47 28 44 45 46 syl3anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) )
48 domentr ⊢ ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) ∧ ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
49 42 47 48 syl2anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
50 49 expr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ) )
51 50 exlimdv ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ) )
52 25 51 mpd ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
53 7 52 exlimddv ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
54 1 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ 𝐵 )
55 difsn ⊢ ( ¬ 𝐶 ∈ 𝐵 → ( 𝐵 ∖ { 𝐶 } ) = 𝐵 )
56 55 breq2d ⊢ ( ¬ 𝐶 ∈ 𝐵 → ( 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ↔ 𝐴 ≼ 𝐵 ) )
57 56 adantl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → ( 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ↔ 𝐴 ≼ 𝐵 ) )
58 54 57 mpbird ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
59 53 58 pm2.61dan ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )