soinfdom

Description: A strict order relation on an infinite set dominates that set. (Contributed by BTernaryTau, 14-Jul-2026)

		Ref	Expression
	Assertion	soinfdom	$⊢ (R Or A \land R \in V \land ω ≼ A) \to A ≼ R$

Proof

Step	Hyp	Ref	Expression
1		infn0	$⊢ ω ≼ A \to A \neq \emptyset$
2		n0	$⊢ A \neq \emptyset \leftrightarrow \exists y y \in A$
3	1 2	sylib	$⊢ ω ≼ A \to \exists y y \in A$
4	3	adantr	$⊢ (ω ≼ A \land (R \in V \land R Or A)) \to \exists y y \in A$
5		infdifsn	$⊢ ω ≼ A \to (A ∖ \{y\}) \approx A$
6	5	ensymd	$⊢ ω ≼ A \to A \approx (A ∖ \{y\})$
7		eldifsn	$⊢ z \in (A ∖ \{y\}) \leftrightarrow (z \in A \land z \neq y)$
8		sotrine	$⊢ (R Or A \land (z \in A \land y \in A)) \to (z \neq y \leftrightarrow (z R y \lor y R z))$
9	8	biimpd	$⊢ (R Or A \land (z \in A \land y \in A)) \to (z \neq y \to (z R y \lor y R z))$
10	9	ancom2s	$⊢ (R Or A \land (y \in A \land z \in A)) \to (z \neq y \to (z R y \lor y R z))$
11	10	expr	$⊢ (R Or A \land y \in A) \to (z \in A \to (z \neq y \to (z R y \lor y R z)))$
12	11	impd	$⊢ (R Or A \land y \in A) \to ((z \in A \land z \neq y) \to (z R y \lor y R z))$
13	7 12	biimtrid	$⊢ (R Or A \land y \in A) \to (z \in (A ∖ \{y\}) \to (z R y \lor y R z))$
14		iftrue	$⊢ z R y \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) = ⟨z, y⟩$
15		df-br	$⊢ z R y \leftrightarrow ⟨z, y⟩ \in R$
16	15	biimpi	$⊢ z R y \to ⟨z, y⟩ \in R$
17	14 16	eqeltrd	$⊢ z R y \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R$
18		df-br	$⊢ y R z \leftrightarrow ⟨y, z⟩ \in R$
19	18	bilani	$⊢ (\neg z R y \land y R z) \to ⟨y, z⟩ \in R$
20		iffalse	$⊢ \neg z R y \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) = ⟨y, z⟩$
21	20	eleq1d	$⊢ \neg z R y \to (if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R \leftrightarrow ⟨y, z⟩ \in R)$
22	21	adantr	$⊢ (\neg z R y \land y R z) \to (if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R \leftrightarrow ⟨y, z⟩ \in R)$
23	19 22	mpbird	$⊢ (\neg z R y \land y R z) \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R$
24	17 23	jaoi3	$⊢ (z R y \lor y R z) \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R$
25	13 24	syl6	$⊢ (R Or A \land y \in A) \to (z \in (A ∖ \{y\}) \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R)$
26	25	ralrimiv	$⊢ (R Or A \land y \in A) \to \forall z \in (A ∖ \{y\}) if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R$
27		eldifsnneq	$⊢ w \in (A ∖ \{y\}) \to \neg w = y$
28	27	neqcomd	$⊢ w \in (A ∖ \{y\}) \to \neg y = w$
29		vex	$⊢ z \in V$
30		vex	$⊢ y \in V$
31	29 30	opth1	$⊢ ⟨z, y⟩ = ⟨w, y⟩ \to z = w$
32	31	a1d	$⊢ ⟨z, y⟩ = ⟨w, y⟩ \to (\neg y = w \to z = w)$
33	29 30	opth	$⊢ ⟨z, y⟩ = ⟨y, w⟩ \leftrightarrow (z = y \land y = w)$
34	33	simprbi	$⊢ ⟨z, y⟩ = ⟨y, w⟩ \to y = w$
35	34	pm2.24d	$⊢ ⟨z, y⟩ = ⟨y, w⟩ \to (\neg y = w \to z = w)$
36	30 29	opth1	$⊢ ⟨y, z⟩ = ⟨w, y⟩ \to y = w$
37	36	pm2.24d	$⊢ ⟨y, z⟩ = ⟨w, y⟩ \to (\neg y = w \to z = w)$
38	30 29	opth	$⊢ ⟨y, z⟩ = ⟨y, w⟩ \leftrightarrow (y = y \land z = w)$
39	38	simprbi	$⊢ ⟨y, z⟩ = ⟨y, w⟩ \to z = w$
40	39	a1d	$⊢ ⟨y, z⟩ = ⟨y, w⟩ \to (\neg y = w \to z = w)$
41	32 35 37 40	jaeqifi	$⊢ if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩) \to (\neg y = w \to z = w)$
42	28 41	syl5com	$⊢ w \in (A ∖ \{y\}) \to (if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩) \to z = w)$
43	42	rgen	$⊢ \forall w \in (A ∖ \{y\}) (if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩) \to z = w)$
44	43	rgenw	$⊢ \forall z \in (A ∖ \{y\}) \forall w \in (A ∖ \{y\}) (if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩) \to z = w)$
45		eqid	$⊢ (z \in (A ∖ \{y\}) ⟼ if (z R y, ⟨z, y⟩, ⟨y, z⟩)) = (z \in (A ∖ \{y\}) ⟼ if (z R y, ⟨z, y⟩, ⟨y, z⟩))$
46		breq1	$⊢ z = w \to (z R y \leftrightarrow w R y)$
47		opeq1	$⊢ z = w \to ⟨z, y⟩ = ⟨w, y⟩$
48		opeq2	$⊢ z = w \to ⟨y, z⟩ = ⟨y, w⟩$
49	46 47 48	ifbieq12d	$⊢ z = w \to if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩)$
50	45 49	f1mpt	$⊢ (z \in (A ∖ \{y\}) ⟼ if (z R y, ⟨z, y⟩, ⟨y, z⟩)) : A ∖ \{y\} \underset{1-1}{⟶} R \leftrightarrow (\forall z \in (A ∖ \{y\}) if (z R y, ⟨z, y⟩, ⟨y, z⟩) \in R \land \forall z \in (A ∖ \{y\}) \forall w \in (A ∖ \{y\}) (if (z R y, ⟨z, y⟩, ⟨y, z⟩) = if (w R y, ⟨w, y⟩, ⟨y, w⟩) \to z = w))$
51	26 44 50	sylanblrc	$⊢ (R Or A \land y \in A) \to (z \in (A ∖ \{y\}) ⟼ if (z R y, ⟨z, y⟩, ⟨y, z⟩)) : A ∖ \{y\} \underset{1-1}{⟶} R$
52		f1domg	$⊢ R \in V \to ((z \in (A ∖ \{y\}) ⟼ if (z R y, ⟨z, y⟩, ⟨y, z⟩)) : A ∖ \{y\} \underset{1-1}{⟶} R \to (A ∖ \{y\}) ≼ R)$
53	51 52	syl5	$⊢ R \in V \to ((R Or A \land y \in A) \to (A ∖ \{y\}) ≼ R)$
54	53	impl	$⊢ ((R \in V \land R Or A) \land y \in A) \to (A ∖ \{y\}) ≼ R$
55		endomtr	$⊢ (A \approx (A ∖ \{y\}) \land (A ∖ \{y\}) ≼ R) \to A ≼ R$
56	6 54 55	syl3an132	$⊢ (ω ≼ A \land (R \in V \land R Or A) \land y \in A) \to A ≼ R$
57	56	3expia	$⊢ (ω ≼ A \land (R \in V \land R Or A)) \to (y \in A \to A ≼ R)$
58	57	exlimdv	$⊢ (ω ≼ A \land (R \in V \land R Or A)) \to (\exists y y \in A \to A ≼ R)$
59	4 58	mpd	$⊢ (ω ≼ A \land (R \in V \land R Or A)) \to A ≼ R$
60	59	ancom2s	$⊢ (ω ≼ A \land (R Or A \land R \in V)) \to A ≼ R$
61	60	ancoms	$⊢ ((R Or A \land R \in V) \land ω ≼ A) \to A ≼ R$
62	61	3impa	$⊢ (R Or A \land R \in V \land ω ≼ A) \to A ≼ R$

Metamath Proof Explorer

Theorem soinfdom

Proof