Theorem fineqvnttrclse 35305

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

Hypotheses

Ref	Expression
fineqvnttrclse.1	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
fineqvnttrclse.2	⊢ 𝐴 = ω

Assertion

Ref	Expression
fineqvnttrclse	⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))

Distinct variable group:   𝑥,𝐴,𝑦

Allowed substitution hints:   𝑅(𝑥,𝑦)

Proof of Theorem fineqvnttrclse

Dummy variables 𝑡 𝑢 𝑤 𝑧 𝑠 𝑑 𝑎 𝑓 𝑛 𝑒 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ominf 9164	. . . . . 6 ⊢ ¬ ω ∈ Fin
2		1onn 8566	. . . . . . 7 ⊢ 1o ∈ ω
3		nnfi 9092	. . . . . . 7 ⊢ (1o ∈ ω → 1o ∈ Fin)
4	2, 3	ax-mp 5	. . . . . 6 ⊢ 1o ∈ Fin
5		difinf 9211	. . . . . 6 ⊢ ((¬ ω ∈ Fin ∧ 1o ∈ Fin) → ¬ (ω ∖ 1o) ∈ Fin)
6	1, 4, 5	mp2an 698	. . . . 5 ⊢ ¬ (ω ∖ 1o) ∈ Fin
7		eleq2 2828	. . . . 5 ⊢ (Fin = V → ((ω ∖ 1o) ∈ Fin ↔ (ω ∖ 1o) ∈ V))
8	6, 7	mtbii 327	. . . 4 ⊢ (Fin = V → ¬ (ω ∖ 1o) ∈ V)
9		difss 4066	. . . . . . . 8 ⊢ (ω ∖ 1o) ⊆ ω
10		fineqvnttrclse.2	. . . . . . . 8 ⊢ 𝐴 = ω
11	9, 10	sseqtrri 3964	. . . . . . 7 ⊢ (ω ∖ 1o) ⊆ 𝐴
12		eldifi 4061	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ ω)
13		eldifn 4062	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ω ∖ 1o) → ¬ 𝑢 ∈ 1o)
14		0lt1o 8429	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 1o
15		eleq1 2827	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ∈ 1o ↔ ∅ ∈ 1o))
16	14, 15	mpbiri 259	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → 𝑢 ∈ 1o)
17	16	necon3bi 2960	. . . . . . . . . . . . 13 ⊢ (¬ 𝑢 ∈ 1o → 𝑢 ≠ ∅)
18	13, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ≠ ∅)
19		nnsuc 7824	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω 𝑢 = suc 𝑛)
20		eqcom 2746	. . . . . . . . . . . . . 14 ⊢ (𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢)
21	20	rexbii 3086	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
22	19, 21	sylib 219	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
23	12, 18, 22	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
24		sucexg 7748	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ V → suc 𝑛 ∈ V)
25	24	elv 3436	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑛 ∈ V
26	25	sucex 7749	. . . . . . . . . . . . . . . 16 ⊢ suc suc 𝑛 ∈ V
27	26	mptex 7167	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V)
29		fineqvnttrclselem1 35302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ ω)
30	29	elexd 3454	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
31	30	ralrimivw 3135	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
32		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})
33	32	fnmpt 6625	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛)
34	31, 33	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ (ω ∖ 1o) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛)
35	34	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛)
36		nnon 7812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
37	12, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ On)
38		eloni 6320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → Ord 𝑢)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → Ord 𝑢)
40	39	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord 𝑢)
41		ordeq 6317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑛 = 𝑢 → (Ord suc 𝑛 ↔ Ord 𝑢))
42	41	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (Ord suc 𝑛 ↔ Ord 𝑢))
43	40, 42	mpbird 258	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord suc 𝑛)
44		0elsuc 7775	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∅ ∈ suc suc 𝑛)
46		simpl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → 𝑢 ∈ (ω ∖ 1o))
47		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = ∅ → (𝑣 +o 𝑑) = (∅ +o 𝑑))
48	47	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∅ → ((𝑣 +o 𝑑) = 𝑢 ↔ (∅ +o 𝑑) = 𝑢))
49	48	rabbidv 3398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∅ → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
50	49	unieqd 4851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = ∅ → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
51		simpl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∅ ∈ suc suc 𝑛)
52		fineqvnttrclselem1 35302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
53	52	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
54	32, 50, 51, 53	fvmptd3 6959	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
55		oa0r 8463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 ∈ On → (∅ +o 𝑑) = 𝑑)
56	55	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ On → ((∅ +o 𝑑) = 𝑢 ↔ 𝑑 = 𝑢))
57	56	rabbiia 3395	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = 𝑢}
58		rabsn 4653	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ 𝑑 = 𝑢} = {𝑢})
59	57, 58	eqtrid 2786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑢})
60	59	unieqd 4851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = ∪ {𝑢})
61		unisnv 4858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ {𝑢} = 𝑢
62	60, 61	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
63	37, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
64	63	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
65	54, 64	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
66	45, 46, 65	syl2anc 590	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
67		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = suc 𝑛 → (𝑣 +o 𝑑) = (suc 𝑛 +o 𝑑))
68	67	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = suc 𝑛 → ((𝑣 +o 𝑑) = 𝑢 ↔ (suc 𝑛 +o 𝑑) = 𝑢))
69	68	rabbidv 3398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = suc 𝑛 → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
70	69	unieqd 4851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = suc 𝑛 → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
71	25	sucid 6394	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
72	71	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → suc 𝑛 ∈ suc suc 𝑛)
73		fineqvnttrclselem1 35302	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} ∈ ω)
74	32, 70, 72, 73	fvmptd3 6959	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
75	74	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
76		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 = 𝑢 → (suc 𝑛 +o 𝑑) = (𝑢 +o 𝑑))
77	76	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑛 = 𝑢 → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
78	77	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
79		oa0 8441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ On → (𝑢 +o ∅) = 𝑢)
80	79	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑢 +o ∅) = 𝑢)
81		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ∅ → (𝑢 +o 𝑑) = (𝑢 +o ∅))
82	81	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = ∅ → ((𝑢 +o 𝑑) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
83	80, 82	syl5ibrcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ → (𝑢 +o 𝑑) = 𝑢))
84		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑑 → (𝑢 +o 𝑠) = (𝑢 +o 𝑑))
85	84	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑑 → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
86		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = ∅ → (𝑢 +o 𝑠) = (𝑢 +o ∅))
87	86	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = ∅ → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
88		ssid 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑢 ⊆ 𝑢
89		oawordeu 8480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ On ∧ 𝑢 ∈ On) ∧ 𝑢 ⊆ 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
90	88, 89	mpan2 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ On ∧ 𝑢 ∈ On) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
91	90	anidms 571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ On → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
92	91	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
93		simp2 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 ∈ On)
94		0elon 6365	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ On
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∅ ∈ On)
96		simp3 1144	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o 𝑑) = 𝑢)
97	79	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o ∅) = 𝑢)
98	85, 87, 92, 93, 95, 96, 97	reu2eqd 3677	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 = ∅)
99	98	3expia 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → ((𝑢 +o 𝑑) = 𝑢 → 𝑑 = ∅))
100	83, 99	impbid 213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
101	100	adantlr 721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
102	78, 101	bitr4d 283	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ 𝑑 = ∅))
103	102	rabbidva 3397	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = ∅})
104	103	unieqd 4851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ 𝑑 = ∅})
105		rabsn 4653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ∈ On → {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅})
106	94, 105	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅}
107	106	unieqi 4850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∪ {∅}
108		0ex 5229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ V
109	108	unisn 4857	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {∅} = ∅
110	107, 109	eqtri 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∅
111	104, 110	eqtrdi 2790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
112	37, 111	sylan 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
113	75, 112	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)
114	66, 113	jca 516	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
115		vex 3435	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
116	115	sucid 6394	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ suc 𝑛
117		eleq2 2828	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑛 = 𝑢 → (𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢))
118	116, 117	mpbii 234	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢)
119		fineqvnttrclse.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
120		oveq2 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑒 → (𝑣 +o 𝑑) = (𝑣 +o 𝑒))
121	120	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑒 → ((𝑣 +o 𝑑) = 𝑢 ↔ (𝑣 +o 𝑒) = 𝑢))
122	121	cbvrabv 3401	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
123	122	unieqi 4850	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
124	123	mpteq2i 5168	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢})
125	119, 10, 124	fineqvnttrclselem3 35304	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ 𝑛 ∈ 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
126	118, 125	sylan2 599	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
127	35, 114, 126	3jca 1134	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛 ∧ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
128		fneq1 6576	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓 Fn suc suc 𝑛 ↔ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛))
129		fveq1 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘∅) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅))
130	129	eqeq1d 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘∅) = 𝑢 ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢))
131		fveq1 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑛) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛))
132	131	eqeq1d 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘suc 𝑛) = ∅ ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
133	130, 132	anbi12d 638	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ↔ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)))
134		fveq1 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎))
135		fveq1 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
136	134, 135	breq12d 5085	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
137	136	ralbidv 3162	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
138	128, 133, 137	3anbi123d 1444	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛 ∧ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))))
139	28, 127, 138	spcedv 3536	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
140	139	ex 413	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → (suc 𝑛 = 𝑢 → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
141	140	reximdv 3154	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → (∃𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
142	23, 141	mpd 15	. . . . . . . . . 10 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
143		brttrcl2 9626	. . . . . . . . . 10 ⊢ (𝑢t++𝑅∅ ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
144	142, 143	sylibr 235	. . . . . . . . 9 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++𝑅∅)
145	119	relopabiv 5763	. . . . . . . . . . . 12 ⊢ Rel 𝑅
146	119	dmeqi 5846	. . . . . . . . . . . . 13 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
147		dmopabss 5860	. . . . . . . . . . . . 13 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} ⊆ 𝐴
148	146, 147	eqsstri 3961	. . . . . . . . . . . 12 ⊢ dom 𝑅 ⊆ 𝐴
149		relssres 5974	. . . . . . . . . . . 12 ⊢ ((Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴) → (𝑅 ↾ 𝐴) = 𝑅)
150	145, 148, 149	mp2an 698	. . . . . . . . . . 11 ⊢ (𝑅 ↾ 𝐴) = 𝑅
151		ttrcleq 9621	. . . . . . . . . . 11 ⊢ ((𝑅 ↾ 𝐴) = 𝑅 → t++(𝑅 ↾ 𝐴) = t++𝑅)
152	150, 151	ax-mp 5	. . . . . . . . . 10 ⊢ t++(𝑅 ↾ 𝐴) = t++𝑅
153	152	breqi 5078	. . . . . . . . 9 ⊢ (𝑢t++(𝑅 ↾ 𝐴)∅ ↔ 𝑢t++𝑅∅)
154	144, 153	sylibr 235	. . . . . . . 8 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++(𝑅 ↾ 𝐴)∅)
155	154	rgen 3055	. . . . . . 7 ⊢ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅
156		ssrab 4002	. . . . . . 7 ⊢ ((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ↔ ((ω ∖ 1o) ⊆ 𝐴 ∧ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅))
157	11, 155, 156	mpbir2an 717	. . . . . 6 ⊢ (ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅}
158		ssexg 5251	. . . . . 6 ⊢ (((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∧ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V) → (ω ∖ 1o) ∈ V)
159	157, 158	mpan 696	. . . . 5 ⊢ ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V → (ω ∖ 1o) ∈ V)
160	159	con3i 154	. . . 4 ⊢ (¬ (ω ∖ 1o) ∈ V → ¬ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V)
161		peano1 7829	. . . . . . 7 ⊢ ∅ ∈ ω
162	161, 10	eleqtrri 2838	. . . . . 6 ⊢ ∅ ∈ 𝐴
163		breq2 5076	. . . . . . . . 9 ⊢ (𝑡 = ∅ → (𝑢t++(𝑅 ↾ 𝐴)𝑡 ↔ 𝑢t++(𝑅 ↾ 𝐴)∅))
164	163	rabbidv 3398	. . . . . . . 8 ⊢ (𝑡 = ∅ → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} = {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅})
165	164	eleq1d 2824	. . . . . . 7 ⊢ (𝑡 = ∅ → ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V ↔ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
166	165	rspcv 3556	. . . . . 6 ⊢ (∅ ∈ 𝐴 → (∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
167	162, 166	ax-mp 5	. . . . 5 ⊢ (∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V)
168	167	con3i 154	. . . 4 ⊢ (¬ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V → ¬ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
169	8, 160, 168	3syl 18	. . 3 ⊢ (Fin = V → ¬ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
170		df-se 5572	. . 3 ⊢ (t++(𝑅 ↾ 𝐴) Se 𝐴 ↔ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
171	169, 170	sylnibr 330	. 2 ⊢ (Fin = V → ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)
172		vex 3435	. . . . . . . . 9 ⊢ 𝑤 ∈ V
173		vex 3435	. . . . . . . . 9 ⊢ 𝑧 ∈ V
174		eleq1w 2822	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
175		eqeq1 2743	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦))
176	174, 175	anbi12d 638	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦)))
177		suceq 6378	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
178	177	eqeq2d 2750	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧))
179	178	anbi2d 636	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧)))
180	172, 173, 176, 179, 119	brab 5485	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
181	180	bilani 505	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
182		simpl 483	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤 ∈ 𝐴)
183	180	biimpri 229	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤𝑅𝑧)
184	182, 183	jca 516	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧))
185	181, 184	impbii 210	. . . . . 6 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
186	185	rabbia2 3394	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} = {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧}
187	173	sucex 7749	. . . . . . . 8 ⊢ suc 𝑧 ∈ V
188	187	eueqi 3650	. . . . . . 7 ⊢ ∃!𝑤 𝑤 = suc 𝑧
189		euabex 5400	. . . . . . 7 ⊢ (∃!𝑤 𝑤 = suc 𝑧 → {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V)
190	188, 189	ax-mp 5	. . . . . 6 ⊢ {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V
191		rabssab 4016	. . . . . 6 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ⊆ {𝑤 ∣ 𝑤 = suc 𝑧}
192	190, 191	ssexi 5250	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ∈ V
193	186, 192	eqeltri 2835	. . . 4 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
194	193	rgenw 3057	. . 3 ⊢ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
195		df-se 5572	. . 3 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V)
196	194, 195	mpbir 232	. 2 ⊢ 𝑅 Se 𝐴
197	171, 196	jctil 524	1 ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃!weu 2572  {cab 2717   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  ∃!wreu 3342  {crab 3391  Vcvv 3431   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4261  {csn 4555  ∪ cuni 4838   class class class wbr 5072  {copab 5134   ↦ cmpt 5153   Se wse 5569  dom cdm 5618   ↾ cres 5620  Rel wrel 5623  Ord word 6309  Oncon0 6310  suc csuc 6312   Fn wfn 6480  ‘cfv 6485  (class class class)co 7356  ωcom 7806  1_oc1o 8388   +_o coa 8392  Fincfn 8883  t++cttrcl 9619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-oadd 8399  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-ttrcl 9620

This theorem is referenced by: (None)