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	28	difexd	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to B ∖ \{x\} \in V$
30		eldifn	$⊢ x \in (B ∖ ran f) \to \neg x \in ran f$
31		disjsn	$⊢ ran f \cap \{x\} = \emptyset \leftrightarrow \neg x \in ran f$
32	30 31	sylibr	$⊢ x \in (B ∖ ran f) \to ran f \cap \{x\} = \emptyset$
33	32	adantl	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \cap \{x\} = \emptyset$
34	9	adantr	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \subseteq B$
35		reldisj	$⊢ ran f \subseteq B \to (ran f \cap \{x\} = \emptyset \leftrightarrow ran f \subseteq B ∖ \{x\})$
36	34 35	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\})$
37	33 36	mpbid	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to ran f \subseteq B ∖ \{x\}$
38		f1ssr	$⊢ (f : A \underset{1-1}{⟶} B \land ran f \subseteq B ∖ \{x\}) \to f : A \underset{1-1}{⟶} B ∖ \{x\}$
39	37 38	syldan	$⊢ (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f)) \to f : A \underset{1-1}{⟶} B ∖ \{x\}$
40	39	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\}$
41		f1dom2g	$⊢ (A \in V \land B ∖ \{x\} \in V \land f : A \underset{1-1}{⟶} B ∖ \{x\}) \to A ≼ (B ∖ \{x\})$
42	27 29 40 41	syl3anc	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to A ≼ (B ∖ \{x\})$
43		eldifi	$⊢ x \in (B ∖ ran f) \to x \in B$
44	43	ad2antll	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to x \in B$
45		simplr	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to C \in B$
46		difsnen	$⊢ (B \in V \land x \in B \land C \in B) \to (B ∖ \{x\}) \approx (B ∖ \{C\})$
47	28 44 45 46	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\})$
48		domentr	$⊢ (A ≼ (B ∖ \{x\}) \land (B ∖ \{x\}) \approx (B ∖ \{C\})) \to A ≼ (B ∖ \{C\})$
49	42 47 48	syl2anc	$⊢ ((A ≺ B \land C \in B) \land (f : A \underset{1-1}{⟶} B \land x \in (B ∖ ran f))) \to A ≼ (B ∖ \{C\})$
50	49	expr	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to (x \in (B ∖ ran f) \to A ≼ (B ∖ \{C\}))$
51	50	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\}))$
52	25 51	mpd	$⊢ ((A ≺ B \land C \in B) \land f : A \underset{1-1}{⟶} B) \to A ≼ (B ∖ \{C\})$
53	7 52	exlimddv	$⊢ (A ≺ B \land C \in B) \to A ≼ (B ∖ \{C\})$
54	1	adantr	$⊢ (A ≺ B \land \neg C \in B) \to A ≼ B$
55		difsn	$⊢ \neg C \in B \to B ∖ \{C\} = B$
56	55	breq2d	$⊢ \neg C \in B \to (A ≼ (B ∖ \{C\}) \leftrightarrow A ≼ B)$
57	56	adantl	$⊢ (A ≺ B \land \neg C \in B) \to (A ≼ (B ∖ \{C\}) \leftrightarrow A ≼ B)$
58	54 57	mpbird	$⊢ (A ≺ B \land \neg C \in B) \to A ≼ (B ∖ \{C\})$
59	53 58	pm2.61dan	$⊢ A ≺ B \to A ≼ (B ∖ \{C\})$

Metamath Proof Explorer

Theorem domdifsn

Proof