sucdom2

Description: Strict dominance of a set over another set implies dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013) (Proof shortened by Mario Carneiro, 27-Apr-2015)

		Ref	Expression
	Assertion	sucdom2	$⊢ A ≺ B \to suc A ≼ B$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2		brdomi	$⊢ A ≼ B \to \exists f f : A \underset{1-1}{⟶} B$
3	1 2	syl	$⊢ A ≺ B \to \exists f f : A \underset{1-1}{⟶} B$
4		relsdom	$⊢ Rel ≺$
5	4	brrelex1i	$⊢ A ≺ B \to A \in V$
6	5	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to A \in V$
7		vex	$⊢ f \in V$
8	7	rnex	$⊢ ran f \in V$
9	8	a1i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \in V$
10		f1f1orn	$⊢ f : A \underset{1-1}{⟶} B \to f : A \underset{1-1 onto}{⟶} ran f$
11	10	adantl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to f : A \underset{1-1 onto}{⟶} ran f$
12		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} ran f \to f : A \underset{1-1}{⟶} ran f$
13	11 12	syl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to f : A \underset{1-1}{⟶} ran f$
14		f1dom2g	$⊢ (A \in V \land ran f \in V \land f : A \underset{1-1}{⟶} ran f) \to A ≼ ran f$
15	6 9 13 14	syl3anc	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to A ≼ ran f$
16		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
17	16	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \neg A \approx B$
18		ssdif0	$⊢ B \subseteq ran f \leftrightarrow B ∖ ran f = \emptyset$
19		simplr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to f : A \underset{1-1}{⟶} B$
20		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
21	20	frnd	$⊢ f : A \underset{1-1}{⟶} B \to ran f \subseteq B$
22	19 21	syl	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to ran f \subseteq B$
23		simpr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to B \subseteq ran f$
24	22 23	eqssd	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to ran f = B$
25		dff1o5	$⊢ f : A \underset{1-1 onto}{⟶} B \leftrightarrow (f : A \underset{1-1}{⟶} B \land ran f = B)$
26	19 24 25	sylanbrc	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to f : A \underset{1-1 onto}{⟶} B$
27		f1oen3g	$⊢ (f \in V \land f : A \underset{1-1 onto}{⟶} B) \to A \approx B$
28	7 26 27	sylancr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to A \approx B$
29	28	ex	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (B \subseteq ran f \to A \approx B)$
30	18 29	syl5bir	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (B ∖ ran f = \emptyset \to A \approx B)$
31	17 30	mtod	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \neg B ∖ ran f = \emptyset$
32		neq0	$⊢ \neg B ∖ ran f = \emptyset \leftrightarrow \exists w w \in (B ∖ ran f)$
33	31 32	sylib	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \exists w w \in (B ∖ ran f)$
34		snssi	$⊢ w \in (B ∖ ran f) \to \{w\} \subseteq B ∖ ran f$
35		vex	$⊢ w \in V$
36		en2sn	$⊢ (A \in V \land w \in V) \to \{A\} \approx \{w\}$
37	6 35 36	sylancl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \{A\} \approx \{w\}$
38	4	brrelex2i	$⊢ A ≺ B \to B \in V$
39	38	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to B \in V$
40		difexg	$⊢ B \in V \to B ∖ ran f \in V$
41		ssdomg	$⊢ B ∖ ran f \in V \to (\{w\} \subseteq B ∖ ran f \to \{w\} ≼ (B ∖ ran f))$
42	39 40 41	3syl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\{w\} \subseteq B ∖ ran f \to \{w\} ≼ (B ∖ ran f))$
43		endomtr	$⊢ (\{A\} \approx \{w\} \land \{w\} ≼ (B ∖ ran f)) \to \{A\} ≼ (B ∖ ran f)$
44	37 42 43	syl6an	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\{w\} \subseteq B ∖ ran f \to \{A\} ≼ (B ∖ ran f))$
45	34 44	syl5	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (w \in (B ∖ ran f) \to \{A\} ≼ (B ∖ ran f))$
46	45	exlimdv	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\exists w w \in (B ∖ ran f) \to \{A\} ≼ (B ∖ ran f))$
47	33 46	mpd	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \{A\} ≼ (B ∖ ran f)$
48		disjdif	$⊢ ran f \cap (B ∖ ran f) = \emptyset$
49	48	a1i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \cap (B ∖ ran f) = \emptyset$
50		undom	$⊢ ((A ≼ ran f \land \{A\} ≼ (B ∖ ran f)) \land ran f \cap (B ∖ ran f) = \emptyset) \to (A \cup \{A\}) ≼ (ran f \cup (B ∖ ran f))$
51	15 47 49 50	syl21anc	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (A \cup \{A\}) ≼ (ran f \cup (B ∖ ran f))$
52		df-suc	$⊢ suc A = A \cup \{A\}$
53	52	a1i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to suc A = A \cup \{A\}$
54		undif2	$⊢ ran f \cup (B ∖ ran f) = ran f \cup B$
55	21	adantl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \subseteq B$
56		ssequn1	$⊢ ran f \subseteq B \leftrightarrow ran f \cup B = B$
57	55 56	sylib	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \cup B = B$
58	54 57	syl5req	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to B = ran f \cup (B ∖ ran f)$
59	51 53 58	3brtr4d	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to suc A ≼ B$
60	3 59	exlimddv	$⊢ A ≺ B \to suc A ≼ B$

Metamath Proof Explorer

Theorem sucdom2

Proof