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 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 𝑥 } ) ∈ V )
30 28 29 syl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ∈ V )
31 eldifn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → ¬ 𝑥 ∈ ran 𝑓 )
32 disjsn ⊢ ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ran 𝑓 )
33 31 32 sylibr ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → ( ran 𝑓 ∩ { 𝑥 } ) = ∅ )
34 33 adantl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ( ran 𝑓 ∩ { 𝑥 } ) = ∅ )
35 9 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ran 𝑓 ⊆ 𝐵 )
36 reldisj ⊢ ( ran 𝑓 ⊆ 𝐵 → ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) )
37 35 36 syl ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ( ( ran 𝑓 ∩ { 𝑥 } ) = ∅ ↔ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) )
38 34 37 mpbid ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) )
39 f1ssr ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ran 𝑓 ⊆ ( 𝐵 ∖ { 𝑥 } ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
40 38 39 syldan ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
41 40 adantl ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) )
42 f1dom2g ⊢ ( ( 𝐴 ∈ V ∧ ( 𝐵 ∖ { 𝑥 } ) ∈ V ∧ 𝑓 : 𝐴 –1-1→ ( 𝐵 ∖ { 𝑥 } ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) )
43 27 30 41 42 syl3anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) )
44 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝑥 ∈ 𝐵 )
45 44 ad2antll ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝑥 ∈ 𝐵 )
46 simplr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐶 ∈ 𝐵 )
47 difsnen ⊢ ( ( 𝐵 ∈ V ∧ 𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) )
48 28 45 46 47 syl3anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) )
49 domentr ⊢ ( ( 𝐴 ≼ ( 𝐵 ∖ { 𝑥 } ) ∧ ( 𝐵 ∖ { 𝑥 } ) ≈ ( 𝐵 ∖ { 𝐶 } ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
50 43 48 49 syl2anc ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) ) ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
51 50 expr ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ) )
52 51 exlimdv ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝐵 ∖ ran 𝑓 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ) )
53 25 52 mpd ⊢ ( ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
54 7 53 exlimddv ⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
55 1 adantr ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ 𝐵 )
56 difsn ⊢ ( ¬ 𝐶 ∈ 𝐵 → ( 𝐵 ∖ { 𝐶 } ) = 𝐵 )
57 56 breq2d ⊢ ( ¬ 𝐶 ∈ 𝐵 → ( 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ↔ 𝐴 ≼ 𝐵 ) )
58 57 adantl ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → ( 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) ↔ 𝐴 ≼ 𝐵 ) )
59 55 58 mpbird ⊢ ( ( 𝐴 ≺ 𝐵 ∧ ¬ 𝐶 ∈ 𝐵 ) → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )
60 54 59 pm2.61dan ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )