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 ( 𝐴𝐵𝐴 ≼ ( 𝐵 ∖ { 𝐶 } ) )