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) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024)

		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		vex	$⊢ f \in V$
5	4	rnex	$⊢ ran f \in V$
6		f1f1orn	$⊢ f : A \underset{1-1}{⟶} B \to f : A \underset{1-1 onto}{⟶} ran f$
7	6	adantl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to f : A \underset{1-1 onto}{⟶} ran f$
8		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} ran f \to f : A \underset{1-1}{⟶} ran f$
9	7 8	syl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to f : A \underset{1-1}{⟶} ran f$
10		f1dom3g	$⊢ (f \in V \land ran f \in V \land f : A \underset{1-1}{⟶} ran f) \to A ≼ ran f$
11	4 5 9 10	mp3an12i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to A ≼ ran f$
12		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
13	12	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \neg A \approx B$
14		ssdif0	$⊢ B \subseteq ran f \leftrightarrow B ∖ ran f = \emptyset$
15		simplr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to f : A \underset{1-1}{⟶} B$
16		f1f	$⊢ f : A \underset{1-1}{⟶} B \to f : A ⟶ B$
17	16	frnd	$⊢ f : A \underset{1-1}{⟶} B \to ran f \subseteq B$
18	15 17	syl	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to ran f \subseteq B$
19		simpr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to B \subseteq ran f$
20	18 19	eqssd	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to ran f = B$
21		dff1o5	$⊢ f : A \underset{1-1 onto}{⟶} B \leftrightarrow (f : A \underset{1-1}{⟶} B \land ran f = B)$
22	15 20 21	sylanbrc	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to f : A \underset{1-1 onto}{⟶} B$
23		f1oen3g	$⊢ (f \in V \land f : A \underset{1-1 onto}{⟶} B) \to A \approx B$
24	4 22 23	sylancr	$⊢ ((A ≺ B \land f : A \underset{1-1}{⟶} B) \land B \subseteq ran f) \to A \approx B$
25	24	ex	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (B \subseteq ran f \to A \approx B)$
26	14 25	biimtrrid	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (B ∖ ran f = \emptyset \to A \approx B)$
27	13 26	mtod	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \neg B ∖ ran f = \emptyset$
28		neq0	$⊢ \neg B ∖ ran f = \emptyset \leftrightarrow \exists w w \in (B ∖ ran f)$
29	27 28	sylib	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \exists w w \in (B ∖ ran f)$
30		snssi	$⊢ w \in (B ∖ ran f) \to \{w\} \subseteq B ∖ ran f$
31		relsdom	$⊢ Rel ≺$
32	31	brrelex1i	$⊢ A ≺ B \to A \in V$
33	32	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to A \in V$
34		vex	$⊢ w \in V$
35		en2sn	$⊢ (A \in V \land w \in V) \to \{A\} \approx \{w\}$
36	33 34 35	sylancl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \{A\} \approx \{w\}$
37	31	brrelex2i	$⊢ A ≺ B \to B \in V$
38	37	adantr	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to B \in V$
39		difexg	$⊢ B \in V \to B ∖ ran f \in V$
40		snfi	$⊢ \{w\} \in Fin$
41		ssdomfi2	$⊢ (\{w\} \in Fin \land B ∖ ran f \in V \land \{w\} \subseteq B ∖ ran f) \to \{w\} ≼ (B ∖ ran f)$
42	40 41	mp3an1	$⊢ (B ∖ ran f \in V \land \{w\} \subseteq B ∖ ran f) \to \{w\} ≼ (B ∖ ran f)$
43	42	ex	$⊢ B ∖ ran f \in V \to (\{w\} \subseteq B ∖ ran f \to \{w\} ≼ (B ∖ ran f))$
44	38 39 43	3syl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\{w\} \subseteq B ∖ ran f \to \{w\} ≼ (B ∖ ran f))$
45		endom	$⊢ \{A\} \approx \{w\} \to \{A\} ≼ \{w\}$
46		domtrfi	$⊢ (\{w\} \in Fin \land \{A\} ≼ \{w\} \land \{w\} ≼ (B ∖ ran f)) \to \{A\} ≼ (B ∖ ran f)$
47	40 46	mp3an1	$⊢ (\{A\} ≼ \{w\} \land \{w\} ≼ (B ∖ ran f)) \to \{A\} ≼ (B ∖ ran f)$
48	45 47	sylan	$⊢ (\{A\} \approx \{w\} \land \{w\} ≼ (B ∖ ran f)) \to \{A\} ≼ (B ∖ ran f)$
49	36 44 48	syl6an	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\{w\} \subseteq B ∖ ran f \to \{A\} ≼ (B ∖ ran f))$
50	30 49	syl5	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (w \in (B ∖ ran f) \to \{A\} ≼ (B ∖ ran f))$
51	50	exlimdv	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (\exists w w \in (B ∖ ran f) \to \{A\} ≼ (B ∖ ran f))$
52	29 51	mpd	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to \{A\} ≼ (B ∖ ran f)$
53		disjdif	$⊢ ran f \cap (B ∖ ran f) = \emptyset$
54	53	a1i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \cap (B ∖ ran f) = \emptyset$
55		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))$
56	11 52 54 55	syl21anc	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to (A \cup \{A\}) ≼ (ran f \cup (B ∖ ran f))$
57		df-suc	$⊢ suc A = A \cup \{A\}$
58	57	a1i	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to suc A = A \cup \{A\}$
59		undif2	$⊢ ran f \cup (B ∖ ran f) = ran f \cup B$
60	17	adantl	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \subseteq B$
61		ssequn1	$⊢ ran f \subseteq B \leftrightarrow ran f \cup B = B$
62	60 61	sylib	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to ran f \cup B = B$
63	59 62	eqtr2id	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to B = ran f \cup (B ∖ ran f)$
64	56 58 63	3brtr4d	$⊢ (A ≺ B \land f : A \underset{1-1}{⟶} B) \to suc A ≼ B$
65	3 64	exlimddv	$⊢ A ≺ B \to suc A ≼ B$

Metamath Proof Explorer

Theorem sucdom2

Proof