fineqvinfep

Description: A counterexample demonstrating that tz9.1 does not hold when all sets are finite and an infinite descending e. -chain exists. (Contributed by BTernaryTau, 18-Feb-2026)

		Ref	Expression
	Hypothesis	fineqvinfep.1	$⊢ A = \{F (\emptyset)\}$
	Assertion	fineqvinfep	$⊢ (Fin = V \land F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to \neg \exists y (A \subseteq y \land Tr y)$

Proof

Step	Hyp	Ref	Expression
1		fineqvinfep.1	$⊢ A = \{F (\emptyset)\}$
2		vex	$⊢ y \in V$
3		eleq2	$⊢ Fin = V \to (y \in Fin \leftrightarrow y \in V)$
4	2 3	mpbiri	$⊢ Fin = V \to y \in Fin$
5	4	3ad2ant1	$⊢ (Fin = V \land F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to y \in Fin$
6		fveq2	$⊢ w = \emptyset \to F (w) = F (\emptyset)$
7	6	eleq1d	$⊢ w = \emptyset \to (F (w) \in y \leftrightarrow F (\emptyset) \in y)$
8		fveq2	$⊢ w = z \to F (w) = F (z)$
9	8	eleq1d	$⊢ w = z \to (F (w) \in y \leftrightarrow F (z) \in y)$
10		fveq2	$⊢ w = suc z \to F (w) = F (suc z)$
11	10	eleq1d	$⊢ w = suc z \to (F (w) \in y \leftrightarrow F (suc z) \in y)$
12		simp2	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to A \subseteq y$
13		fvex	$⊢ F (\emptyset) \in V$
14	13	snid	$⊢ F (\emptyset) \in \{F (\emptyset)\}$
15	14 1	eleqtrri	$⊢ F (\emptyset) \in A$
16	15	a1i	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to F (\emptyset) \in A$
17	12 16	sseldd	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to F (\emptyset) \in y$
18		3simpb	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to (\forall x \in ω F (suc x) \in F (x) \land Tr y)$
19		suceq	$⊢ x = z \to suc x = suc z$
20	19	fveq2d	$⊢ x = z \to F (suc x) = F (suc z)$
21		fveq2	$⊢ x = z \to F (x) = F (z)$
22	20 21	eleq12d	$⊢ x = z \to (F (suc x) \in F (x) \leftrightarrow F (suc z) \in F (z))$
23	22	rspcv	$⊢ z \in ω \to (\forall x \in ω F (suc x) \in F (x) \to F (suc z) \in F (z))$
24		trel	$⊢ Tr y \to ((F (suc z) \in F (z) \land F (z) \in y) \to F (suc z) \in y)$
25	24	expd	$⊢ Tr y \to (F (suc z) \in F (z) \to (F (z) \in y \to F (suc z) \in y))$
26	25	com12	$⊢ F (suc z) \in F (z) \to (Tr y \to (F (z) \in y \to F (suc z) \in y))$
27	23 26	syl6	$⊢ z \in ω \to (\forall x \in ω F (suc x) \in F (x) \to (Tr y \to (F (z) \in y \to F (suc z) \in y)))$
28	27	impd	$⊢ z \in ω \to ((\forall x \in ω F (suc x) \in F (x) \land Tr y) \to (F (z) \in y \to F (suc z) \in y))$
29	18 28	syl5	$⊢ z \in ω \to ((\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to (F (z) \in y \to F (suc z) \in y))$
30	7 9 11 17 29	finds2	$⊢ w \in ω \to ((\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to F (w) \in y)$
31	30	com12	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to (w \in ω \to F (w) \in y)$
32	31	ralrimiv	$⊢ (\forall x \in ω F (suc x) \in F (x) \land A \subseteq y \land Tr y) \to \forall w \in ω F (w) \in y$
33	32	3expib	$⊢ \forall x \in ω F (suc x) \in F (x) \to ((A \subseteq y \land Tr y) \to \forall w \in ω F (w) \in y)$
34	33	adantl	$⊢ (F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to ((A \subseteq y \land Tr y) \to \forall w \in ω F (w) \in y)$
35		f1fun	$⊢ F : ω \underset{1-1}{⟶} V \to Fun F$
36		f1dm	$⊢ F : ω \underset{1-1}{⟶} V \to dom F = ω$
37	36	eqimsscd	$⊢ F : ω \underset{1-1}{⟶} V \to ω \subseteq dom F$
38		funimass4	$⊢ (Fun F \land ω \subseteq dom F) \to (F [ω] \subseteq y \leftrightarrow \forall w \in ω F (w) \in y)$
39	35 37 38	syl2anc	$⊢ F : ω \underset{1-1}{⟶} V \to (F [ω] \subseteq y \leftrightarrow \forall w \in ω F (w) \in y)$
40	39	adantr	$⊢ (F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to (F [ω] \subseteq y \leftrightarrow \forall w \in ω F (w) \in y)$
41	34 40	sylibrd	$⊢ (F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to ((A \subseteq y \land Tr y) \to F [ω] \subseteq y)$
42		ominf	$⊢ \neg ω \in Fin$
43		f1fn	$⊢ F : ω \underset{1-1}{⟶} V \to F Fn ω$
44		fnima	$⊢ F Fn ω \to F [ω] = ran F$
45	43 44	syl	$⊢ F : ω \underset{1-1}{⟶} V \to F [ω] = ran F$
46	45	eqimsscd	$⊢ F : ω \underset{1-1}{⟶} V \to ran F \subseteq F [ω]$
47		f1ssr	$⊢ (F : ω \underset{1-1}{⟶} V \land ran F \subseteq F [ω]) \to F : ω \underset{1-1}{⟶} F [ω]$
48	46 47	mpdan	$⊢ F : ω \underset{1-1}{⟶} V \to F : ω \underset{1-1}{⟶} F [ω]$
49		f1fi	$⊢ (F [ω] \in Fin \land F : ω \underset{1-1}{⟶} F [ω]) \to ω \in Fin$
50	48 49	sylan2	$⊢ (F [ω] \in Fin \land F : ω \underset{1-1}{⟶} V) \to ω \in Fin$
51	50	ancoms	$⊢ (F : ω \underset{1-1}{⟶} V \land F [ω] \in Fin) \to ω \in Fin$
52	42 51	mto	$⊢ \neg (F : ω \underset{1-1}{⟶} V \land F [ω] \in Fin)$
53	52	imnani	$⊢ F : ω \underset{1-1}{⟶} V \to \neg F [ω] \in Fin$
54		ssfi	$⊢ (y \in Fin \land F [ω] \subseteq y) \to F [ω] \in Fin$
55	54	ancoms	$⊢ (F [ω] \subseteq y \land y \in Fin) \to F [ω] \in Fin$
56	55	con3i	$⊢ \neg F [ω] \in Fin \to \neg (F [ω] \subseteq y \land y \in Fin)$
57		imnan	$⊢ (F [ω] \subseteq y \to \neg y \in Fin) \leftrightarrow \neg (F [ω] \subseteq y \land y \in Fin)$
58	56 57	sylibr	$⊢ \neg F [ω] \in Fin \to (F [ω] \subseteq y \to \neg y \in Fin)$
59	53 58	syl	$⊢ F : ω \underset{1-1}{⟶} V \to (F [ω] \subseteq y \to \neg y \in Fin)$
60	59	adantr	$⊢ (F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to (F [ω] \subseteq y \to \neg y \in Fin)$
61	41 60	syld	$⊢ (F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to ((A \subseteq y \land Tr y) \to \neg y \in Fin)$
62	61	3adant1	$⊢ (Fin = V \land F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to ((A \subseteq y \land Tr y) \to \neg y \in Fin)$
63	5 62	mt2d	$⊢ (Fin = V \land F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to \neg (A \subseteq y \land Tr y)$
64	63	nexdv	$⊢ (Fin = V \land F : ω \underset{1-1}{⟶} V \land \forall x \in ω F (suc x) \in F (x)) \to \neg \exists y (A \subseteq y \land Tr y)$

Metamath Proof Explorer

Theorem fineqvinfep

Proof