noinfep

Description: Using the Axiom of Regularity in the form zfregfr , show that there are no infinite descending e. -chains. Proposition 7.34 of TakeutiZaring p. 44. (Contributed by NM, 26-Jan-2006) (Revised by Mario Carneiro, 22-Mar-2013)

		Ref	Expression
	Assertion	noinfep	$⊢ \exists x \in ω F (suc x) \notin F (x)$

Proof

Step	Hyp	Ref	Expression
1		omex	$⊢ ω \in V$
2	1	mptex	$⊢ (w \in ω ⟼ F (w)) \in V$
3	2	rnex	$⊢ ran (w \in ω ⟼ F (w)) \in V$
4		zfregfr	$⊢ E Fr ran (w \in ω ⟼ F (w))$
5		ssid	$⊢ ran (w \in ω ⟼ F (w)) \subseteq ran (w \in ω ⟼ F (w))$
6		dmmptg	$⊢ \forall w \in ω F (w) \in V \to dom (w \in ω ⟼ F (w)) = ω$
7		fvexd	$⊢ w \in ω \to F (w) \in V$
8	6 7	mprg	$⊢ dom (w \in ω ⟼ F (w)) = ω$
9		peano1	$⊢ \emptyset \in ω$
10	9	ne0ii	$⊢ ω \neq \emptyset$
11	8 10	eqnetri	$⊢ dom (w \in ω ⟼ F (w)) \neq \emptyset$
12		dm0rn0	$⊢ dom (w \in ω ⟼ F (w)) = \emptyset \leftrightarrow ran (w \in ω ⟼ F (w)) = \emptyset$
13	12	necon3bii	$⊢ dom (w \in ω ⟼ F (w)) \neq \emptyset \leftrightarrow ran (w \in ω ⟼ F (w)) \neq \emptyset$
14	11 13	mpbi	$⊢ ran (w \in ω ⟼ F (w)) \neq \emptyset$
15		fri	$⊢ ((ran (w \in ω ⟼ F (w)) \in V \land E Fr ran (w \in ω ⟼ F (w))) \land (ran (w \in ω ⟼ F (w)) \subseteq ran (w \in ω ⟼ F (w)) \land ran (w \in ω ⟼ F (w)) \neq \emptyset)) \to \exists y \in ran (w \in ω ⟼ F (w)) \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y$
16	3 4 5 14 15	mp4an	$⊢ \exists y \in ran (w \in ω ⟼ F (w)) \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y$
17		fvex	$⊢ F (w) \in V$
18		eqid	$⊢ (w \in ω ⟼ F (w)) = (w \in ω ⟼ F (w))$
19	17 18	fnmpti	$⊢ (w \in ω ⟼ F (w)) Fn ω$
20		fvelrnb	$⊢ (w \in ω ⟼ F (w)) Fn ω \to (y \in ran (w \in ω ⟼ F (w)) \leftrightarrow \exists x \in ω (w \in ω ⟼ F (w)) (x) = y)$
21	19 20	ax-mp	$⊢ y \in ran (w \in ω ⟼ F (w)) \leftrightarrow \exists x \in ω (w \in ω ⟼ F (w)) (x) = y$
22		peano2	$⊢ x \in ω \to suc x \in ω$
23		fveq2	$⊢ w = suc x \to F (w) = F (suc x)$
24		fvex	$⊢ F (suc x) \in V$
25	23 18 24	fvmpt	$⊢ suc x \in ω \to (w \in ω ⟼ F (w)) (suc x) = F (suc x)$
26	22 25	syl	$⊢ x \in ω \to (w \in ω ⟼ F (w)) (suc x) = F (suc x)$
27		fnfvelrn	$⊢ ((w \in ω ⟼ F (w)) Fn ω \land suc x \in ω) \to (w \in ω ⟼ F (w)) (suc x) \in ran (w \in ω ⟼ F (w))$
28	19 22 27	sylancr	$⊢ x \in ω \to (w \in ω ⟼ F (w)) (suc x) \in ran (w \in ω ⟼ F (w))$
29	26 28	eqeltrrd	$⊢ x \in ω \to F (suc x) \in ran (w \in ω ⟼ F (w))$
30		epel	$⊢ z E y \leftrightarrow z \in y$
31		eleq1	$⊢ z = F (suc x) \to (z \in y \leftrightarrow F (suc x) \in y)$
32	30 31	bitrid	$⊢ z = F (suc x) \to (z E y \leftrightarrow F (suc x) \in y)$
33	32	notbid	$⊢ z = F (suc x) \to (\neg z E y \leftrightarrow \neg F (suc x) \in y)$
34		df-nel	$⊢ F (suc x) \notin y \leftrightarrow \neg F (suc x) \in y$
35	33 34	bitr4di	$⊢ z = F (suc x) \to (\neg z E y \leftrightarrow F (suc x) \notin y)$
36	35	rspccv	$⊢ \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to (F (suc x) \in ran (w \in ω ⟼ F (w)) \to F (suc x) \notin y)$
37	29 36	syl5com	$⊢ x \in ω \to (\forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to F (suc x) \notin y)$
38		fveq2	$⊢ w = x \to F (w) = F (x)$
39		fvex	$⊢ F (x) \in V$
40	38 18 39	fvmpt	$⊢ x \in ω \to (w \in ω ⟼ F (w)) (x) = F (x)$
41		eqeq1	$⊢ (w \in ω ⟼ F (w)) (x) = y \to ((w \in ω ⟼ F (w)) (x) = F (x) \leftrightarrow y = F (x))$
42	40 41	syl5ibcom	$⊢ x \in ω \to ((w \in ω ⟼ F (w)) (x) = y \to y = F (x))$
43		neleq2	$⊢ y = F (x) \to (F (suc x) \notin y \leftrightarrow F (suc x) \notin F (x))$
44	43	biimpd	$⊢ y = F (x) \to (F (suc x) \notin y \to F (suc x) \notin F (x))$
45	42 44	syl6	$⊢ x \in ω \to ((w \in ω ⟼ F (w)) (x) = y \to (F (suc x) \notin y \to F (suc x) \notin F (x)))$
46	45	com23	$⊢ x \in ω \to (F (suc x) \notin y \to ((w \in ω ⟼ F (w)) (x) = y \to F (suc x) \notin F (x)))$
47	37 46	syldc	$⊢ \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to (x \in ω \to ((w \in ω ⟼ F (w)) (x) = y \to F (suc x) \notin F (x)))$
48	47	reximdvai	$⊢ \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to (\exists x \in ω (w \in ω ⟼ F (w)) (x) = y \to \exists x \in ω F (suc x) \notin F (x))$
49	21 48	syl5bi	$⊢ \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to (y \in ran (w \in ω ⟼ F (w)) \to \exists x \in ω F (suc x) \notin F (x))$
50	49	com12	$⊢ y \in ran (w \in ω ⟼ F (w)) \to (\forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to \exists x \in ω F (suc x) \notin F (x))$
51	50	rexlimiv	$⊢ \exists y \in ran (w \in ω ⟼ F (w)) \forall z \in ran (w \in ω ⟼ F (w)) \neg z E y \to \exists x \in ω F (suc x) \notin F (x)$
52	16 51	ax-mp	$⊢ \exists x \in ω F (suc x) \notin F (x)$

Metamath Proof Explorer

Theorem noinfep

Proof