onnseq

Description: There are no length _om decreasing sequences in the ordinals. See also noinfep for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015)

		Ref	Expression
	Assertion	onnseq	$⊢ F (\emptyset) \in On \to \exists x \in ω \neg F (suc x) \in F (x)$

Proof

Step	Hyp	Ref	Expression
1		epweon	$⊢ E We On$
2		fveq2	$⊢ y = \emptyset \to F (y) = F (\emptyset)$
3	2	eleq1d	$⊢ y = \emptyset \to (F (y) \in On \leftrightarrow F (\emptyset) \in On)$
4		fveq2	$⊢ y = z \to F (y) = F (z)$
5	4	eleq1d	$⊢ y = z \to (F (y) \in On \leftrightarrow F (z) \in On)$
6		fveq2	$⊢ y = suc z \to F (y) = F (suc z)$
7	6	eleq1d	$⊢ y = suc z \to (F (y) \in On \leftrightarrow F (suc z) \in On)$
8		simpl	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to F (\emptyset) \in On$
9		suceq	$⊢ x = z \to suc x = suc z$
10	9	fveq2d	$⊢ x = z \to F (suc x) = F (suc z)$
11		fveq2	$⊢ x = z \to F (x) = F (z)$
12	10 11	eleq12d	$⊢ x = z \to (F (suc x) \in F (x) \leftrightarrow F (suc z) \in F (z))$
13	12	rspcv	$⊢ z \in ω \to (\forall x \in ω F (suc x) \in F (x) \to F (suc z) \in F (z))$
14		onelon	$⊢ (F (z) \in On \land F (suc z) \in F (z)) \to F (suc z) \in On$
15	14	expcom	$⊢ F (suc z) \in F (z) \to (F (z) \in On \to F (suc z) \in On)$
16	13 15	syl6	$⊢ z \in ω \to (\forall x \in ω F (suc x) \in F (x) \to (F (z) \in On \to F (suc z) \in On))$
17	16	adantld	$⊢ z \in ω \to ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to (F (z) \in On \to F (suc z) \in On))$
18	3 5 7 8 17	finds2	$⊢ y \in ω \to ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to F (y) \in On)$
19	18	com12	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to (y \in ω \to F (y) \in On)$
20	19	ralrimiv	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to \forall y \in ω F (y) \in On$
21		eqid	$⊢ (y \in ω ⟼ F (y)) = (y \in ω ⟼ F (y))$
22	21	fmpt	$⊢ \forall y \in ω F (y) \in On \leftrightarrow (y \in ω ⟼ F (y)) : ω ⟶ On$
23	20 22	sylib	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to (y \in ω ⟼ F (y)) : ω ⟶ On$
24	23	frnd	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to ran (y \in ω ⟼ F (y)) \subseteq On$
25		peano1	$⊢ \emptyset \in ω$
26	23	fdmd	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to dom (y \in ω ⟼ F (y)) = ω$
27	25 26	eleqtrrid	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to \emptyset \in dom (y \in ω ⟼ F (y))$
28	27	ne0d	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to dom (y \in ω ⟼ F (y)) \neq \emptyset$
29		dm0rn0	$⊢ dom (y \in ω ⟼ F (y)) = \emptyset \leftrightarrow ran (y \in ω ⟼ F (y)) = \emptyset$
30	29	necon3bii	$⊢ dom (y \in ω ⟼ F (y)) \neq \emptyset \leftrightarrow ran (y \in ω ⟼ F (y)) \neq \emptyset$
31	28 30	sylib	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to ran (y \in ω ⟼ F (y)) \neq \emptyset$
32		wefrc	$⊢ (E We On \land ran (y \in ω ⟼ F (y)) \subseteq On \land ran (y \in ω ⟼ F (y)) \neq \emptyset) \to \exists z \in ran (y \in ω ⟼ F (y)) ran (y \in ω ⟼ F (y)) \cap z = \emptyset$
33	1 24 31 32	mp3an2i	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to \exists z \in ran (y \in ω ⟼ F (y)) ran (y \in ω ⟼ F (y)) \cap z = \emptyset$
34		fvex	$⊢ F (w) \in V$
35	34	rgenw	$⊢ \forall w \in ω F (w) \in V$
36		fveq2	$⊢ y = w \to F (y) = F (w)$
37	36	cbvmptv	$⊢ (y \in ω ⟼ F (y)) = (w \in ω ⟼ F (w))$
38		ineq2	$⊢ z = F (w) \to ran (y \in ω ⟼ F (y)) \cap z = ran (y \in ω ⟼ F (y)) \cap F (w)$
39	38	eqeq1d	$⊢ z = F (w) \to (ran (y \in ω ⟼ F (y)) \cap z = \emptyset \leftrightarrow ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset)$
40	37 39	rexrnmptw	$⊢ \forall w \in ω F (w) \in V \to (\exists z \in ran (y \in ω ⟼ F (y)) ran (y \in ω ⟼ F (y)) \cap z = \emptyset \leftrightarrow \exists w \in ω ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset)$
41	35 40	ax-mp	$⊢ \exists z \in ran (y \in ω ⟼ F (y)) ran (y \in ω ⟼ F (y)) \cap z = \emptyset \leftrightarrow \exists w \in ω ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset$
42	33 41	sylib	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to \exists w \in ω ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset$
43		peano2	$⊢ w \in ω \to suc w \in ω$
44	43	adantl	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to suc w \in ω$
45		eqid	$⊢ F (suc w) = F (suc w)$
46		fveq2	$⊢ y = suc w \to F (y) = F (suc w)$
47	46	rspceeqv	$⊢ (suc w \in ω \land F (suc w) = F (suc w)) \to \exists y \in ω F (suc w) = F (y)$
48	44 45 47	sylancl	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to \exists y \in ω F (suc w) = F (y)$
49		fvex	$⊢ F (suc w) \in V$
50	21	elrnmpt	$⊢ F (suc w) \in V \to (F (suc w) \in ran (y \in ω ⟼ F (y)) \leftrightarrow \exists y \in ω F (suc w) = F (y))$
51	49 50	ax-mp	$⊢ F (suc w) \in ran (y \in ω ⟼ F (y)) \leftrightarrow \exists y \in ω F (suc w) = F (y)$
52	48 51	sylibr	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to F (suc w) \in ran (y \in ω ⟼ F (y))$
53		suceq	$⊢ x = w \to suc x = suc w$
54	53	fveq2d	$⊢ x = w \to F (suc x) = F (suc w)$
55		fveq2	$⊢ x = w \to F (x) = F (w)$
56	54 55	eleq12d	$⊢ x = w \to (F (suc x) \in F (x) \leftrightarrow F (suc w) \in F (w))$
57	56	rspccva	$⊢ (\forall x \in ω F (suc x) \in F (x) \land w \in ω) \to F (suc w) \in F (w)$
58	57	adantll	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to F (suc w) \in F (w)$
59		inelcm	$⊢ (F (suc w) \in ran (y \in ω ⟼ F (y)) \land F (suc w) \in F (w)) \to ran (y \in ω ⟼ F (y)) \cap F (w) \neq \emptyset$
60	52 58 59	syl2anc	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to ran (y \in ω ⟼ F (y)) \cap F (w) \neq \emptyset$
61	60	neneqd	$⊢ ((F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \land w \in ω) \to \neg ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset$
62	61	nrexdv	$⊢ (F (\emptyset) \in On \land \forall x \in ω F (suc x) \in F (x)) \to \neg \exists w \in ω ran (y \in ω ⟼ F (y)) \cap F (w) = \emptyset$
63	42 62	pm2.65da	$⊢ F (\emptyset) \in On \to \neg \forall x \in ω F (suc x) \in F (x)$
64		rexnal	$⊢ \exists x \in ω \neg F (suc x) \in F (x) \leftrightarrow \neg \forall x \in ω F (suc x) \in F (x)$
65	63 64	sylibr	$⊢ F (\emptyset) \in On \to \exists x \in ω \neg F (suc x) \in F (x)$

Metamath Proof Explorer

Theorem onnseq

Proof