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	$⊢ A ≺ B \to A ≼ (B ∖ \{C\})$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2		relsdom	$⊢ Rel ≺$
3	2	brrelex2i	$⊢ A ≺ B \to B \in V$
4		brdomg	$⊢ B \in V \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
5	3 4	syl	$⊢ A ≺ B \to (A ≼ B \leftrightarrow \exists f f : A \underset{1-1}{⟶} B)$
6	1 5	mpbid	$⊢ A ≺ B \to \exists f f : A \underset{1-1}{⟶} B$
7	6	adantr	$⊢ (A ≺ B \land C \in B) \to \exists f f : A \underset{1-1}{⟶} B$
8		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
9	8	frnd	$⊢ f : A \underset{1-1}{⟶} B \to ran f \subseteq B$
10	9	adantl	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to ran f \subseteq B$
11		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
12	11	ad2antrr	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to \neg A \approx B$
13		vex	$⊢ f \in V$
14		dff1o5	$⊢ f : A \underset{1-1 onto}{⟶} B \leftrightarrow (f : A \underset{1-1}{⟶} B \land ran f = B)$
15	14	biimpri	$⊢ (f : A \underset{1-1}{⟶} B \land ran f = B) \to f : A \underset{1-1 onto}{⟶} B$
16		f1oen3g	$⊢ (f \in V \land f : A \underset{1-1 onto}{⟶} B) \to A \approx B$
17	13 15 16	sylancr	$⊢ (f : A \underset{1-1}{⟶} B \land ran f = B) \to A \approx B$
18	17	ex	$⊢ f : A \underset{1-1}{⟶} B \to (ran f = B \to A \approx B)$
19	18	necon3bd	$⊢ f : A \underset{1-1}{⟶} B \to (\neg A \approx B \to ran f \neq B)$
20	19	adantl	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to (\neg A \approx B \to ran f \neq B)$
21	12 20	mpd	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to ran f \neq B$
22		pssdifn0	$⊢ (ran f \subseteq B \land ran f \neq B) \to B ∖ ran f \neq \emptyset$
23	10 21 22	syl2anc	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to B ∖ ran f \neq \emptyset$
24		n0	$⊢ B ∖ ran f \neq \emptyset \leftrightarrow \exists x x \in (B ∖ ran f)$
25	23 24	sylib	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to \exists x x \in (B ∖ ran f)$
26	2	brrelex1i	$⊢ A ≺ B \to A \in V$
27	26	ad2antrr	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to A \in V$
28	3	ad2antrr	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to B \in V$
29		difexg	$⊢ B \in V \to B ∖ \{x\} \in V$
30	28 29	syl	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to B ∖ \{x\} \in V$
31		eldifn	$⊢ x \in (B ∖ ran f) \to \neg x \in ran f$
32		disjsn	$⊢ ran f \cap \{x\} = \emptyset \leftrightarrow \neg x \in ran f$
33	31 32	sylibr	$⊢ x \in (B ∖ ran f) \to ran f \cap \{x\} = \emptyset$
34	33	adantl	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \cap \{x\} = \emptyset$
35	9	adantr	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \subseteq B$
36		reldisj	$⊢ ran f \subseteq B \to (ran f \cap \{x\} = \emptyset \leftrightarrow ran f \subseteq B ∖ \{x\})$
37	35 36	syl	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to (ran f \cap \{x\} = \emptyset \leftrightarrow ran f \subseteq B ∖ \{x\})$
38	34 37	mpbid	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \subseteq B ∖ \{x\}$
39		f1ssr	$⊢ (f : A \underset{1-1}{⟶} B \land ran f \subseteq B ∖ \{x\}) \to f : A \underset{1-1}{⟶} B ∖ \{x\}$
40	38 39	syldan	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to f : A \underset{1-1}{⟶} B ∖ \{x\}$
41	40	adantl	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to f : A \underset{1-1}{⟶} B ∖ \{x\}$
42		f1dom2g	$⊢ (A \in V \land B ∖ \{x\} \in V \land f : A \underset{1-1}{⟶} B ∖ \{x\}) \to A ≼ (B ∖ \{x\})$
43	27 30 41 42	syl3anc	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to A ≼ (B ∖ \{x\})$
44		eldifi	$⊢ x \in (B ∖ ran f) \to x \in B$
45	44	ad2antll	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to x \in B$
46		simplr	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to C \in B$
47		difsnen	$⊢ (B \in V \land x \in B \land C \in B) \to (B ∖ \{x\}) \approx (B ∖ \{C\})$
48	28 45 46 47	syl3anc	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to (B ∖ \{x\}) \approx (B ∖ \{C\})$
49		domentr	$⊢ (A ≼ (B ∖ \{x\}) \land (B ∖ \{x\}) \approx (B ∖ \{C\})) \to A ≼ (B ∖ \{C\})$
50	43 48 49	syl2anc	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to A ≼ (B ∖ \{C\})$
51	50	expr	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to (x \in (B ∖ ran f) \to A ≼ (B ∖ \{C\}))$
52	51	exlimdv	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to (\exists x x \in (B ∖ ran f) \to A ≼ (B ∖ \{C\}))$
53	25 52	mpd	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to A ≼ (B ∖ \{C\})$
54	7 53	exlimddv	$⊢ (A ≺ B \land C \in B) \to A ≼ (B ∖ \{C\})$
55	1	adantr	$⊢ (A ≺ B \land \neg C \in B) \to A ≼ B$
56		difsn	$⊢ \neg C \in B \to B ∖ \{C\} = B$
57	56	breq2d	$⊢ \neg C \in B \to (A ≼ (B ∖ \{C\}) \leftrightarrow A ≼ B)$
58	57	adantl	$⊢ (A ≺ B \land \neg C \in B) \to (A ≼ (B ∖ \{C\}) \leftrightarrow A ≼ B)$
59	55 58	mpbird	$⊢ (A ≺ B \land \neg C \in B) \to A ≼ (B ∖ \{C\})$
60	54 59	pm2.61dan	$⊢ A ≺ B \to A ≼ (B ∖ \{C\})$

Metamath Proof Explorer

Theorem domdifsn

Proof