Theorem fineqvnttrclse 35268

Description: A counterexample demonstrating that ttrclse 9648 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 9174	. . . . . 6 ⊢ ¬ ω ∈ Fin
2		1onn 8576	. . . . . . 7 ⊢ 1o ∈ ω
3		nnfi 9102	. . . . . . 7 ⊢ (1o ∈ ω → 1o ∈ Fin)
4	2, 3	ax-mp 5	. . . . . 6 ⊢ 1o ∈ Fin
5		difinf 9221	. . . . . 6 ⊢ ((¬ ω ∈ Fin ∧ 1o ∈ Fin) → ¬ (ω ∖ 1o) ∈ Fin)
6	1, 4, 5	mp2an 693	. . . . 5 ⊢ ¬ (ω ∖ 1o) ∈ Fin
7		eleq2 2825	. . . . 5 ⊢ (Fin = V → ((ω ∖ 1o) ∈ Fin ↔ (ω ∖ 1o) ∈ V))
8	6, 7	mtbii 326	. . . 4 ⊢ (Fin = V → ¬ (ω ∖ 1o) ∈ V)
9		difss 4076	. . . . . . . 8 ⊢ (ω ∖ 1o) ⊆ ω
10		fineqvnttrclse.2	. . . . . . . 8 ⊢ 𝐴 = ω
11	9, 10	sseqtrri 3971	. . . . . . 7 ⊢ (ω ∖ 1o) ⊆ 𝐴
12		eldifi 4071	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ ω)
13		eldifn 4072	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ω ∖ 1o) → ¬ 𝑢 ∈ 1o)
14		0lt1o 8439	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 1o
15		eleq1 2824	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ∈ 1o ↔ ∅ ∈ 1o))
16	14, 15	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → 𝑢 ∈ 1o)
17	16	necon3bi 2958	. . . . . . . . . . . . 13 ⊢ (¬ 𝑢 ∈ 1o → 𝑢 ≠ ∅)
18	13, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ≠ ∅)
19		nnsuc 7835	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω 𝑢 = suc 𝑛)
20		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ (𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢)
21	20	rexbii 3084	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
22	19, 21	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
23	12, 18, 22	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
24		sucexg 7759	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ V → suc 𝑛 ∈ V)
25	24	elv 3434	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑛 ∈ V
26	25	sucex 7760	. . . . . . . . . . . . . . . 16 ⊢ suc suc 𝑛 ∈ V
27	26	mptex 7178	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V)
29		fineqvnttrclselem1 35265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ ω)
30	29	elexd 3453	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
31	30	ralrimivw 3133	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
32		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})
33	32	fnmpt 6638	. . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛)
36		nnon 7823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
37	12, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ On)
38		eloni 6333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → Ord 𝑢)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → Ord 𝑢)
40	39	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord 𝑢)
41		ordeq 6330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑛 = 𝑢 → (Ord suc 𝑛 ↔ Ord 𝑢))
42	41	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (Ord suc 𝑛 ↔ Ord 𝑢))
43	40, 42	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord suc 𝑛)
44		0elsuc 7786	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∅ ∈ suc suc 𝑛)
46		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → 𝑢 ∈ (ω ∖ 1o))
47		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = ∅ → (𝑣 +o 𝑑) = (∅ +o 𝑑))
48	47	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∅ → ((𝑣 +o 𝑑) = 𝑢 ↔ (∅ +o 𝑑) = 𝑢))
49	48	rabbidv 3396	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∅ → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
50	49	unieqd 4863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = ∅ → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
51		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∅ ∈ suc suc 𝑛)
52		fineqvnttrclselem1 35265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
53	52	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
54	32, 50, 51, 53	fvmptd3 6971	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
55		oa0r 8473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 ∈ On → (∅ +o 𝑑) = 𝑑)
56	55	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ On → ((∅ +o 𝑑) = 𝑢 ↔ 𝑑 = 𝑢))
57	56	rabbiia 3393	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = 𝑢}
58		rabsn 4665	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ 𝑑 = 𝑢} = {𝑢})
59	57, 58	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑢})
60	59	unieqd 4863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = ∪ {𝑢})
61		unisnv 4870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ {𝑢} = 𝑢
62	60, 61	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
63	37, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
64	63	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
65	54, 64	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
66	45, 46, 65	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
67		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = suc 𝑛 → (𝑣 +o 𝑑) = (suc 𝑛 +o 𝑑))
68	67	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = suc 𝑛 → ((𝑣 +o 𝑑) = 𝑢 ↔ (suc 𝑛 +o 𝑑) = 𝑢))
69	68	rabbidv 3396	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = suc 𝑛 → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
70	69	unieqd 4863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = suc 𝑛 → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
71	25	sucid 6407	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
72	71	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → suc 𝑛 ∈ suc suc 𝑛)
73		fineqvnttrclselem1 35265	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} ∈ ω)
74	32, 70, 72, 73	fvmptd3 6971	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
75	74	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
76		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 = 𝑢 → (suc 𝑛 +o 𝑑) = (𝑢 +o 𝑑))
77	76	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑛 = 𝑢 → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
78	77	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
79		oa0 8451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ On → (𝑢 +o ∅) = 𝑢)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑢 +o ∅) = 𝑢)
81		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ∅ → (𝑢 +o 𝑑) = (𝑢 +o ∅))
82	81	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = ∅ → ((𝑢 +o 𝑑) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
83	80, 82	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ → (𝑢 +o 𝑑) = 𝑢))
84		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑑 → (𝑢 +o 𝑠) = (𝑢 +o 𝑑))
85	84	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑑 → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
86		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = ∅ → (𝑢 +o 𝑠) = (𝑢 +o ∅))
87	86	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = ∅ → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
88		ssid 3944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑢 ⊆ 𝑢
89		oawordeu 8490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ On ∧ 𝑢 ∈ On) ∧ 𝑢 ⊆ 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
90	88, 89	mpan2 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ On ∧ 𝑢 ∈ On) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
91	90	anidms 566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ On → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
92	91	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
93		simp2 1138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 ∈ On)
94		0elon 6378	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ On
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∅ ∈ On)
96		simp3 1139	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o 𝑑) = 𝑢)
97	79	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o ∅) = 𝑢)
98	85, 87, 92, 93, 95, 96, 97	reu2eqd 3682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 = ∅)
99	98	3expia 1122	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → ((𝑢 +o 𝑑) = 𝑢 → 𝑑 = ∅))
100	83, 99	impbid 212	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
101	100	adantlr 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
102	78, 101	bitr4d 282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ 𝑑 = ∅))
103	102	rabbidva 3395	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = ∅})
104	103	unieqd 4863	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ 𝑑 = ∅})
105		rabsn 4665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ∈ On → {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅})
106	94, 105	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅}
107	106	unieqi 4862	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∪ {∅}
108		0ex 5242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ V
109	108	unisn 4869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {∅} = ∅
110	107, 109	eqtri 2759	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∅
111	104, 110	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
112	37, 111	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
113	75, 112	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)
114	66, 113	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
115		vex 3433	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
116	115	sucid 6407	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ suc 𝑛
117		eleq2 2825	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑛 = 𝑢 → (𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢))
118	116, 117	mpbii 233	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢)
119		fineqvnttrclse.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
120		oveq2 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑒 → (𝑣 +o 𝑑) = (𝑣 +o 𝑒))
121	120	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑒 → ((𝑣 +o 𝑑) = 𝑢 ↔ (𝑣 +o 𝑒) = 𝑢))
122	121	cbvrabv 3399	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
123	122	unieqi 4862	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
124	123	mpteq2i 5181	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢})
125	119, 10, 124	fineqvnttrclselem3 35267	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ 𝑛 ∈ 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
126	118, 125	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
127	35, 114, 126	3jca 1129	. . . . . . . . . . . . . 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 6589	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓 Fn suc suc 𝑛 ↔ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛))
129		fveq1 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘∅) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅))
130	129	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘∅) = 𝑢 ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢))
131		fveq1 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑛) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛))
132	131	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘suc 𝑛) = ∅ ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
133	130, 132	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ↔ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)))
134		fveq1 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎))
135		fveq1 6839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
136	134, 135	breq12d 5098	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
137	136	ralbidv 3160	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
138	128, 133, 137	3anbi123d 1439	. . . . . . . . . . . . . 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 3540	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
140	139	ex 412	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → (suc 𝑛 = 𝑢 → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
141	140	reximdv 3152	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → (∃𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
142	23, 141	mpd 15	. . . . . . . . . 10 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
143		brttrcl2 9635	. . . . . . . . . 10 ⊢ (𝑢t++𝑅∅ ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
144	142, 143	sylibr 234	. . . . . . . . 9 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++𝑅∅)
145	119	relopabiv 5776	. . . . . . . . . . . 12 ⊢ Rel 𝑅
146	119	dmeqi 5859	. . . . . . . . . . . . 13 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
147		dmopabss 5873	. . . . . . . . . . . . 13 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} ⊆ 𝐴
148	146, 147	eqsstri 3968	. . . . . . . . . . . 12 ⊢ dom 𝑅 ⊆ 𝐴
149		relssres 5987	. . . . . . . . . . . 12 ⊢ ((Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴) → (𝑅 ↾ 𝐴) = 𝑅)
150	145, 148, 149	mp2an 693	. . . . . . . . . . 11 ⊢ (𝑅 ↾ 𝐴) = 𝑅
151		ttrcleq 9630	. . . . . . . . . . 11 ⊢ ((𝑅 ↾ 𝐴) = 𝑅 → t++(𝑅 ↾ 𝐴) = t++𝑅)
152	150, 151	ax-mp 5	. . . . . . . . . 10 ⊢ t++(𝑅 ↾ 𝐴) = t++𝑅
153	152	breqi 5091	. . . . . . . . 9 ⊢ (𝑢t++(𝑅 ↾ 𝐴)∅ ↔ 𝑢t++𝑅∅)
154	144, 153	sylibr 234	. . . . . . . 8 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++(𝑅 ↾ 𝐴)∅)
155	154	rgen 3053	. . . . . . 7 ⊢ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅
156		ssrab 4011	. . . . . . 7 ⊢ ((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ↔ ((ω ∖ 1o) ⊆ 𝐴 ∧ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅))
157	11, 155, 156	mpbir2an 712	. . . . . 6 ⊢ (ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅}
158		ssexg 5264	. . . . . 6 ⊢ (((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∧ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V) → (ω ∖ 1o) ∈ V)
159	157, 158	mpan 691	. . . . 5 ⊢ ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V → (ω ∖ 1o) ∈ V)
160	159	con3i 154	. . . 4 ⊢ (¬ (ω ∖ 1o) ∈ V → ¬ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V)
161		peano1 7840	. . . . . . 7 ⊢ ∅ ∈ ω
162	161, 10	eleqtrri 2835	. . . . . 6 ⊢ ∅ ∈ 𝐴
163		breq2 5089	. . . . . . . . 9 ⊢ (𝑡 = ∅ → (𝑢t++(𝑅 ↾ 𝐴)𝑡 ↔ 𝑢t++(𝑅 ↾ 𝐴)∅))
164	163	rabbidv 3396	. . . . . . . 8 ⊢ (𝑡 = ∅ → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} = {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅})
165	164	eleq1d 2821	. . . . . . 7 ⊢ (𝑡 = ∅ → ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V ↔ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
166	165	rspcv 3560	. . . . . 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 5585	. . 3 ⊢ (t++(𝑅 ↾ 𝐴) Se 𝐴 ↔ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
171	169, 170	sylnibr 329	. 2 ⊢ (Fin = V → ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)
172		vex 3433	. . . . . . . . . 10 ⊢ 𝑤 ∈ V
173		vex 3433	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
174		eleq1w 2819	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
175		eqeq1 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦))
176	174, 175	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦)))
177		suceq 6391	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
178	177	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧))
179	178	anbi2d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧)))
180	172, 173, 176, 179, 119	brab 5498	. . . . . . . . 9 ⊢ (𝑤𝑅𝑧 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
181	180	biimpi 216	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 → (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
182	181	adantl 481	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
183		simpl 482	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤 ∈ 𝐴)
184	180	biimpri 228	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤𝑅𝑧)
185	183, 184	jca 511	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧))
186	182, 185	impbii 209	. . . . . 6 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
187	186	rabbia2 3392	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} = {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧}
188	173	sucex 7760	. . . . . . . 8 ⊢ suc 𝑧 ∈ V
189	188	eueqi 3655	. . . . . . 7 ⊢ ∃!𝑤 𝑤 = suc 𝑧
190		euabex 5413	. . . . . . 7 ⊢ (∃!𝑤 𝑤 = suc 𝑧 → {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V)
191	189, 190	ax-mp 5	. . . . . 6 ⊢ {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V
192		rabssab 4025	. . . . . 6 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ⊆ {𝑤 ∣ 𝑤 = suc 𝑧}
193	191, 192	ssexi 5263	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ∈ V
194	187, 193	eqeltri 2832	. . . 4 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
195	194	rgenw 3055	. . 3 ⊢ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
196		df-se 5585	. . 3 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V)
197	195, 196	mpbir 231	. 2 ⊢ 𝑅 Se 𝐴
198	171, 197	jctil 519	1 ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃!weu 2568  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  ∃!wreu 3340  {crab 3389  Vcvv 3429   ∖ cdif 3886   ⊆ wss 3889  ∅c0 4273  {csn 4567  ∪ cuni 4850   class class class wbr 5085  {copab 5147   ↦ cmpt 5166   Se wse 5582  dom cdm 5631   ↾ cres 5633  Rel wrel 5636  Ord word 6322  Oncon0 6323  suc csuc 6325   Fn wfn 6493  ‘cfv 6498  (class class class)co 7367  ωcom 7817  1_oc1o 8398   +_o coa 8402  Fincfn 8893  t++cttrcl 9628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-oadd 8409  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-ttrcl 9629

This theorem is referenced by: (None)