fineqvnttrclse

Description: A counterexample demonstrating that ttrclse does not hold when all sets are finite. (Contributed by BTernaryTau, 12-Jan-2026)

	Ref	Expression
Hypotheses	fineqvnttrclse.1	$⊢ R = \{⟨x, y⟩ \| (x \in A \land x = suc y)\}$
	fineqvnttrclse.2	$⊢ A = ω$
Assertion	fineqvnttrclse	$⊢ Fin = V \to (R Se A \land \neg t++ ({R ↾}_{A}) Se A)$

Proof

Step	Hyp	Ref	Expression
1		fineqvnttrclse.1	$⊢ R = \{⟨x, y⟩ \| (x \in A \land x = suc y)\}$
2		fineqvnttrclse.2	$⊢ A = ω$
3		ominf	$⊢ \neg ω \in Fin$
4		1onn	$⊢ 1_{𝑜} \in ω$
5		nnfi	$⊢ 1_{𝑜} \in ω \to 1_{𝑜} \in Fin$
6	4 5	ax-mp	$⊢ 1_{𝑜} \in Fin$
7		difinf	$⊢ (\neg ω \in Fin \land 1_{𝑜} \in Fin) \to \neg ω ∖ 1_{𝑜} \in Fin$
8	3 6 7	mp2an	$⊢ \neg ω ∖ 1_{𝑜} \in Fin$
9		eleq2	$⊢ Fin = V \to (ω ∖ 1_{𝑜} \in Fin \leftrightarrow ω ∖ 1_{𝑜} \in V)$
10	8 9	mtbii	$⊢ Fin = V \to \neg ω ∖ 1_{𝑜} \in V$
11		difss	$⊢ ω ∖ 1_{𝑜} \subseteq ω$
12	11 2	sseqtrri	$⊢ ω ∖ 1_{𝑜} \subseteq A$
13		eldifi	$⊢ u \in (ω ∖ 1_{𝑜}) \to u \in ω$
14		eldifn	$⊢ u \in (ω ∖ 1_{𝑜}) \to \neg u \in 1_{𝑜}$
15		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
16		eleq1	$⊢ u = \emptyset \to (u \in 1_{𝑜} \leftrightarrow \emptyset \in 1_{𝑜})$
17	15 16	mpbiri	$⊢ u = \emptyset \to u \in 1_{𝑜}$
18	17	necon3bi	$⊢ \neg u \in 1_{𝑜} \to u \neq \emptyset$
19	14 18	syl	$⊢ u \in (ω ∖ 1_{𝑜}) \to u \neq \emptyset$
20		nnsuc	$⊢ (u \in ω \land u \neq \emptyset) \to \exists n \in ω u = suc n$
21		eqcom	$⊢ u = suc n \leftrightarrow suc n = u$
22	21	rexbii	$⊢ \exists n \in ω u = suc n \leftrightarrow \exists n \in ω suc n = u$
23	20 22	sylib	$⊢ (u \in ω \land u \neq \emptyset) \to \exists n \in ω suc n = u$
24	13 19 23	syl2anc	$⊢ u \in (ω ∖ 1_{𝑜}) \to \exists n \in ω suc n = u$
25		sucexg	$⊢ n \in V \to suc n \in V$
26	25	elv	$⊢ suc n \in V$
27	26	sucex	$⊢ suc suc n \in V$
28	27	mptex	$⊢ (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \in V$
29	28	a1i	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \in V$
30		fineqvnttrclselem1	$⊢ u \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| v +_{𝑜} d = u\} \in ω$
31	30	elexd	$⊢ u \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| v +_{𝑜} d = u\} \in V$
32	31	ralrimivw	$⊢ u \in (ω ∖ 1_{𝑜}) \to \forall v \in suc suc n ⋃ \{d \in On \| v +_{𝑜} d = u\} \in V$
33		eqid	$⊢ (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\})$
34	33	fnmpt	$⊢ \forall v \in suc suc n ⋃ \{d \in On \| v +_{𝑜} d = u\} \in V \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n$
35	32 34	syl	$⊢ u \in (ω ∖ 1_{𝑜}) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n$
36	35	adantr	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n$
37		nnon	$⊢ u \in ω \to u \in On$
38	13 37	syl	$⊢ u \in (ω ∖ 1_{𝑜}) \to u \in On$
39		eloni	$⊢ u \in On \to Ord u$
40	38 39	syl	$⊢ u \in (ω ∖ 1_{𝑜}) \to Ord u$
41	40	adantr	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to Ord u$
42		ordeq	$⊢ suc n = u \to (Ord suc n \leftrightarrow Ord u)$
43	42	adantl	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (Ord suc n \leftrightarrow Ord u)$
44	41 43	mpbird	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to Ord suc n$
45		0elsuc	$⊢ Ord suc n \to \emptyset \in suc suc n$
46	44 45	syl	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to \emptyset \in suc suc n$
47		simpl	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to u \in (ω ∖ 1_{𝑜})$
48		oveq1	$⊢ v = \emptyset \to v +_{𝑜} d = \emptyset +_{𝑜} d$
49	48	eqeq1d	$⊢ v = \emptyset \to (v +_{𝑜} d = u \leftrightarrow \emptyset +_{𝑜} d = u)$
50	49	rabbidv	$⊢ v = \emptyset \to \{d \in On \| v +_{𝑜} d = u\} = \{d \in On \| \emptyset +_{𝑜} d = u\}$
51	50	unieqd	$⊢ v = \emptyset \to ⋃ \{d \in On \| v +_{𝑜} d = u\} = ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\}$
52		simpl	$⊢ (\emptyset \in suc suc n \land u \in (ω ∖ 1_{𝑜})) \to \emptyset \in suc suc n$
53		fineqvnttrclselem1	$⊢ u \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} \in ω$
54	53	adantl	$⊢ (\emptyset \in suc suc n \land u \in (ω ∖ 1_{𝑜})) \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} \in ω$
55	33 51 52 54	fvmptd3	$⊢ (\emptyset \in suc suc n \land u \in (ω ∖ 1_{𝑜})) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\}$
56		oa0r	$⊢ d \in On \to \emptyset +_{𝑜} d = d$
57	56	eqeq1d	$⊢ d \in On \to (\emptyset +_{𝑜} d = u \leftrightarrow d = u)$
58	57	rabbiia	$⊢ \{d \in On \| \emptyset +_{𝑜} d = u\} = \{d \in On \| d = u\}$
59		rabsn	$⊢ u \in On \to \{d \in On \| d = u\} = \{u\}$
60	58 59	eqtrid	$⊢ u \in On \to \{d \in On \| \emptyset +_{𝑜} d = u\} = \{u\}$
61	60	unieqd	$⊢ u \in On \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} = ⋃ \{u\}$
62		unisnv	$⊢ ⋃ \{u\} = u$
63	61 62	eqtrdi	$⊢ u \in On \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} = u$
64	38 63	syl	$⊢ u \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} = u$
65	64	adantl	$⊢ (\emptyset \in suc suc n \land u \in (ω ∖ 1_{𝑜})) \to ⋃ \{d \in On \| \emptyset +_{𝑜} d = u\} = u$
66	55 65	eqtrd	$⊢ (\emptyset \in suc suc n \land u \in (ω ∖ 1_{𝑜})) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u$
67	46 47 66	syl2anc	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u$
68		oveq1	$⊢ v = suc n \to v +_{𝑜} d = suc n +_{𝑜} d$
69	68	eqeq1d	$⊢ v = suc n \to (v +_{𝑜} d = u \leftrightarrow suc n +_{𝑜} d = u)$
70	69	rabbidv	$⊢ v = suc n \to \{d \in On \| v +_{𝑜} d = u\} = \{d \in On \| suc n +_{𝑜} d = u\}$
71	70	unieqd	$⊢ v = suc n \to ⋃ \{d \in On \| v +_{𝑜} d = u\} = ⋃ \{d \in On \| suc n +_{𝑜} d = u\}$
72	26	sucid	$⊢ suc n \in suc suc n$
73	72	a1i	$⊢ u \in (ω ∖ 1_{𝑜}) \to suc n \in suc suc n$
74		fineqvnttrclselem1	$⊢ u \in (ω ∖ 1_{𝑜}) \to ⋃ \{d \in On \| suc n +_{𝑜} d = u\} \in ω$
75	33 71 73 74	fvmptd3	$⊢ u \in (ω ∖ 1_{𝑜}) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = ⋃ \{d \in On \| suc n +_{𝑜} d = u\}$
76	75	adantr	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = ⋃ \{d \in On \| suc n +_{𝑜} d = u\}$
77		oveq1	$⊢ suc n = u \to suc n +_{𝑜} d = u +_{𝑜} d$
78	77	eqeq1d	$⊢ suc n = u \to (suc n +_{𝑜} d = u \leftrightarrow u +_{𝑜} d = u)$
79	78	ad2antlr	$⊢ ((u \in On \land suc n = u) \land d \in On) \to (suc n +_{𝑜} d = u \leftrightarrow u +_{𝑜} d = u)$
80		oa0	$⊢ u \in On \to u +_{𝑜} \emptyset = u$
81	80	adantr	$⊢ (u \in On \land d \in On) \to u +_{𝑜} \emptyset = u$
82		oveq2	$⊢ d = \emptyset \to u +_{𝑜} d = u +_{𝑜} \emptyset$
83	82	eqeq1d	$⊢ d = \emptyset \to (u +_{𝑜} d = u \leftrightarrow u +_{𝑜} \emptyset = u)$
84	81 83	syl5ibrcom	$⊢ (u \in On \land d \in On) \to (d = \emptyset \to u +_{𝑜} d = u)$
85		oveq2	$⊢ s = d \to u +_{𝑜} s = u +_{𝑜} d$
86	85	eqeq1d	$⊢ s = d \to (u +_{𝑜} s = u \leftrightarrow u +_{𝑜} d = u)$
87		oveq2	$⊢ s = \emptyset \to u +_{𝑜} s = u +_{𝑜} \emptyset$
88	87	eqeq1d	$⊢ s = \emptyset \to (u +_{𝑜} s = u \leftrightarrow u +_{𝑜} \emptyset = u)$
89		ssid	$⊢ u \subseteq u$
90		oawordeu	$⊢ ((u \in On \land u \in On) \land u \subseteq u) \to \exists! s \in On u +_{𝑜} s = u$
91	89 90	mpan2	$⊢ (u \in On \land u \in On) \to \exists! s \in On u +_{𝑜} s = u$
92	91	anidms	$⊢ u \in On \to \exists! s \in On u +_{𝑜} s = u$
93	92	3ad2ant1	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to \exists! s \in On u +_{𝑜} s = u$
94		simp2	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to d \in On$
95		0elon	$⊢ \emptyset \in On$
96	95	a1i	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to \emptyset \in On$
97		simp3	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to u +_{𝑜} d = u$
98	80	3ad2ant1	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to u +_{𝑜} \emptyset = u$
99	86 88 93 94 96 97 98	reu2eqd	$⊢ (u \in On \land d \in On \land u +_{𝑜} d = u) \to d = \emptyset$
100	99	3expia	$⊢ (u \in On \land d \in On) \to (u +_{𝑜} d = u \to d = \emptyset)$
101	84 100	impbid	$⊢ (u \in On \land d \in On) \to (d = \emptyset \leftrightarrow u +_{𝑜} d = u)$
102	101	adantlr	$⊢ ((u \in On \land suc n = u) \land d \in On) \to (d = \emptyset \leftrightarrow u +_{𝑜} d = u)$
103	79 102	bitr4d	$⊢ ((u \in On \land suc n = u) \land d \in On) \to (suc n +_{𝑜} d = u \leftrightarrow d = \emptyset)$
104	103	rabbidva	$⊢ (u \in On \land suc n = u) \to \{d \in On \| suc n +_{𝑜} d = u\} = \{d \in On \| d = \emptyset\}$
105	104	unieqd	$⊢ (u \in On \land suc n = u) \to ⋃ \{d \in On \| suc n +_{𝑜} d = u\} = ⋃ \{d \in On \| d = \emptyset\}$
106		rabsn	$⊢ \emptyset \in On \to \{d \in On \| d = \emptyset\} = \{\emptyset\}$
107	95 106	ax-mp	$⊢ \{d \in On \| d = \emptyset\} = \{\emptyset\}$
108	107	unieqi	$⊢ ⋃ \{d \in On \| d = \emptyset\} = ⋃ \{\emptyset\}$
109		0ex	$⊢ \emptyset \in V$
110	109	unisn	$⊢ ⋃ \{\emptyset\} = \emptyset$
111	108 110	eqtri	$⊢ ⋃ \{d \in On \| d = \emptyset\} = \emptyset$
112	105 111	eqtrdi	$⊢ (u \in On \land suc n = u) \to ⋃ \{d \in On \| suc n +_{𝑜} d = u\} = \emptyset$
113	38 112	sylan	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to ⋃ \{d \in On \| suc n +_{𝑜} d = u\} = \emptyset$
114	76 113	eqtrd	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset$
115	67 114	jca	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u \land (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset)$
116		vex	$⊢ n \in V$
117	116	sucid	$⊢ n \in suc n$
118		eleq2	$⊢ suc n = u \to (n \in suc n \leftrightarrow n \in u)$
119	117 118	mpbii	$⊢ suc n = u \to n \in u$
120		oveq2	$⊢ d = e \to v +_{𝑜} d = v +_{𝑜} e$
121	120	eqeq1d	$⊢ d = e \to (v +_{𝑜} d = u \leftrightarrow v +_{𝑜} e = u)$
122	121	cbvrabv	$⊢ \{d \in On \| v +_{𝑜} d = u\} = \{e \in On \| v +_{𝑜} e = u\}$
123	122	unieqi	$⊢ ⋃ \{d \in On \| v +_{𝑜} d = u\} = ⋃ \{e \in On \| v +_{𝑜} e = u\}$
124	123	mpteq2i	$⊢ (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) = (v \in suc suc n ⟼ ⋃ \{e \in On \| v +_{𝑜} e = u\})$
125	1 2 124	fineqvnttrclselem3	$⊢ (u \in (ω ∖ 1_{𝑜}) \land n \in u) \to \forall a \in suc n (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a)$
126	119 125	sylan2	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to \forall a \in suc n (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a)$
127	36 115 126	3jca	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n \land ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u \land (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset) \land \forall a \in suc n (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a))$
128		fneq1	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to (f Fn suc suc n \leftrightarrow (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n)$
129		fveq1	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to f (\emptyset) = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset)$
130	129	eqeq1d	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to (f (\emptyset) = u \leftrightarrow (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u)$
131		fveq1	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to f (suc n) = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n)$
132	131	eqeq1d	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to (f (suc n) = \emptyset \leftrightarrow (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset)$
133	130 132	anbi12d	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to ((f (\emptyset) = u \land f (suc n) = \emptyset) \leftrightarrow ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u \land (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset))$
134		fveq1	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to f (a) = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a)$
135		fveq1	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to f (suc a) = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a)$
136	134 135	breq12d	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to (f (a) R f (suc a) \leftrightarrow (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a))$
137	136	ralbidv	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to (\forall a \in suc n f (a) R f (suc a) \leftrightarrow \forall a \in suc n (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a))$
138	128 133 137	3anbi123d	$⊢ f = (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) \to ((f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a)) \leftrightarrow ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) Fn suc suc n \land ((v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (\emptyset) = u \land (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc n) = \emptyset) \land \forall a \in suc n (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (a) R (v \in suc suc n ⟼ ⋃ \{d \in On \| v +_{𝑜} d = u\}) (suc a)))$
139	29 127 138	spcedv	$⊢ (u \in (ω ∖ 1_{𝑜}) \land suc n = u) \to \exists f (f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a))$
140	139	ex	$⊢ u \in (ω ∖ 1_{𝑜}) \to (suc n = u \to \exists f (f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a)))$
141	140	reximdv	$⊢ u \in (ω ∖ 1_{𝑜}) \to (\exists n \in ω suc n = u \to \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a)))$
142	24 141	mpd	$⊢ u \in (ω ∖ 1_{𝑜}) \to \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a))$
143		brttrcl2	$⊢ u t++ R \emptyset \leftrightarrow \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = u \land f (suc n) = \emptyset) \land \forall a \in suc n f (a) R f (suc a))$
144	142 143	sylibr	$⊢ u \in (ω ∖ 1_{𝑜}) \to u t++ R \emptyset$
145	1	relopabiv	$⊢ Rel R$
146	1	dmeqi	$⊢ dom R = dom \{⟨x, y⟩ \| (x \in A \land x = suc y)\}$
147		dmopabss	$⊢ dom \{⟨x, y⟩ \| (x \in A \land x = suc y)\} \subseteq A$
148	146 147	eqsstri	$⊢ dom R \subseteq A$
149		relssres	$⊢ (Rel R \land dom R \subseteq A) \to {R ↾}_{A} = R$
150	145 148 149	mp2an	$⊢ {R ↾}_{A} = R$
151		ttrcleq	$⊢ {R ↾}_{A} = R \to t++ ({R ↾}_{A}) = t++ R$
152	150 151	ax-mp	$⊢ t++ ({R ↾}_{A}) = t++ R$
153	152	breqi	$⊢ u t++ ({R ↾}_{A}) \emptyset \leftrightarrow u t++ R \emptyset$
154	144 153	sylibr	$⊢ u \in (ω ∖ 1_{𝑜}) \to u t++ ({R ↾}_{A}) \emptyset$
155	154	rgen	$⊢ \forall u \in (ω ∖ 1_{𝑜}) u t++ ({R ↾}_{A}) \emptyset$
156		ssrab	$⊢ ω ∖ 1_{𝑜} \subseteq \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \leftrightarrow (ω ∖ 1_{𝑜} \subseteq A \land \forall u \in (ω ∖ 1_{𝑜}) u t++ ({R ↾}_{A}) \emptyset)$
157	12 155 156	mpbir2an	$⊢ ω ∖ 1_{𝑜} \subseteq \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\}$
158		ssexg	$⊢ (ω ∖ 1_{𝑜} \subseteq \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \land \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V) \to ω ∖ 1_{𝑜} \in V$
159	157 158	mpan	$⊢ \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V \to ω ∖ 1_{𝑜} \in V$
160	159	con3i	$⊢ \neg ω ∖ 1_{𝑜} \in V \to \neg \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V$
161		peano1	$⊢ \emptyset \in ω$
162	161 2	eleqtrri	$⊢ \emptyset \in A$
163		breq2	$⊢ t = \emptyset \to (u t++ ({R ↾}_{A}) t \leftrightarrow u t++ ({R ↾}_{A}) \emptyset)$
164	163	rabbidv	$⊢ t = \emptyset \to \{u \in A \| u t++ ({R ↾}_{A}) t\} = \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\}$
165	164	eleq1d	$⊢ t = \emptyset \to (\{u \in A \| u t++ ({R ↾}_{A}) t\} \in V \leftrightarrow \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V)$
166	165	rspcv	$⊢ \emptyset \in A \to (\forall t \in A \{u \in A \| u t++ ({R ↾}_{A}) t\} \in V \to \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V)$
167	162 166	ax-mp	$⊢ \forall t \in A \{u \in A \| u t++ ({R ↾}_{A}) t\} \in V \to \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V$
168	167	con3i	$⊢ \neg \{u \in A \| u t++ ({R ↾}_{A}) \emptyset\} \in V \to \neg \forall t \in A \{u \in A \| u t++ ({R ↾}_{A}) t\} \in V$
169	10 160 168	3syl	$⊢ Fin = V \to \neg \forall t \in A \{u \in A \| u t++ ({R ↾}_{A}) t\} \in V$
170		df-se	$⊢ t++ ({R ↾}_{A}) Se A \leftrightarrow \forall t \in A \{u \in A \| u t++ ({R ↾}_{A}) t\} \in V$
171	169 170	sylnibr	$⊢ Fin = V \to \neg t++ ({R ↾}_{A}) Se A$
172		vex	$⊢ w \in V$
173		vex	$⊢ z \in V$
174		eleq1w	$⊢ x = w \to (x \in A \leftrightarrow w \in A)$
175		eqeq1	$⊢ x = w \to (x = suc y \leftrightarrow w = suc y)$
176	174 175	anbi12d	$⊢ x = w \to ((x \in A \land x = suc y) \leftrightarrow (w \in A \land w = suc y))$
177		suceq	$⊢ y = z \to suc y = suc z$
178	177	eqeq2d	$⊢ y = z \to (w = suc y \leftrightarrow w = suc z)$
179	178	anbi2d	$⊢ y = z \to ((w \in A \land w = suc y) \leftrightarrow (w \in A \land w = suc z))$
180	172 173 176 179 1	brab	$⊢ w R z \leftrightarrow (w \in A \land w = suc z)$
181	180	biimpi	$⊢ w R z \to (w \in A \land w = suc z)$
182	181	adantl	$⊢ (w \in A \land w R z) \to (w \in A \land w = suc z)$
183		simpl	$⊢ (w \in A \land w = suc z) \to w \in A$
184	180	biimpri	$⊢ (w \in A \land w = suc z) \to w R z$
185	183 184	jca	$⊢ (w \in A \land w = suc z) \to (w \in A \land w R z)$
186	182 185	impbii	$⊢ (w \in A \land w R z) \leftrightarrow (w \in A \land w = suc z)$
187	186	rabbia2	$⊢ \{w \in A \| w R z\} = \{w \in A \| w = suc z\}$
188	173	sucex	$⊢ suc z \in V$
189	188	eueqi	$⊢ \exists! w w = suc z$
190		euabex	$⊢ \exists! w w = suc z \to \{w \| w = suc z\} \in V$
191	189 190	ax-mp	$⊢ \{w \| w = suc z\} \in V$
192		rabssab	$⊢ \{w \in A \| w = suc z\} \subseteq \{w \| w = suc z\}$
193	191 192	ssexi	$⊢ \{w \in A \| w = suc z\} \in V$
194	187 193	eqeltri	$⊢ \{w \in A \| w R z\} \in V$
195	194	rgenw	$⊢ \forall z \in A \{w \in A \| w R z\} \in V$
196		df-se	$⊢ R Se A \leftrightarrow \forall z \in A \{w \in A \| w R z\} \in V$
197	195 196	mpbir	$⊢ R Se A$
198	171 197	jctil	$⊢ Fin = V \to (R Se A \land \neg t++ ({R ↾}_{A}) Se A)$

Metamath Proof Explorer

Theorem fineqvnttrclse

Proof