Theorem fineqvnttrclse 35287

Description: A counterexample demonstrating that ttrclse 9642 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 9168	. . . . . 6 ⊢ ¬ ω ∈ Fin
2		1onn 8570	. . . . . . 7 ⊢ 1o ∈ ω
3		nnfi 9096	. . . . . . 7 ⊢ (1o ∈ ω → 1o ∈ Fin)
4	2, 3	ax-mp 5	. . . . . 6 ⊢ 1o ∈ Fin
5		difinf 9215	. . . . . 6 ⊢ ((¬ ω ∈ Fin ∧ 1o ∈ Fin) → ¬ (ω ∖ 1o) ∈ Fin)
6	1, 4, 5	mp2an 693	. . . . 5 ⊢ ¬ (ω ∖ 1o) ∈ Fin
7		eleq2 2826	. . . . 5 ⊢ (Fin = V → ((ω ∖ 1o) ∈ Fin ↔ (ω ∖ 1o) ∈ V))
8	6, 7	mtbii 326	. . . 4 ⊢ (Fin = V → ¬ (ω ∖ 1o) ∈ V)
9		difss 4077	. . . . . . . 8 ⊢ (ω ∖ 1o) ⊆ ω
10		fineqvnttrclse.2	. . . . . . . 8 ⊢ 𝐴 = ω
11	9, 10	sseqtrri 3972	. . . . . . 7 ⊢ (ω ∖ 1o) ⊆ 𝐴
12		eldifi 4072	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ ω)
13		eldifn 4073	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ω ∖ 1o) → ¬ 𝑢 ∈ 1o)
14		0lt1o 8433	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 1o
15		eleq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ∈ 1o ↔ ∅ ∈ 1o))
16	14, 15	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → 𝑢 ∈ 1o)
17	16	necon3bi 2959	. . . . . . . . . . . . 13 ⊢ (¬ 𝑢 ∈ 1o → 𝑢 ≠ ∅)
18	13, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ≠ ∅)
19		nnsuc 7829	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω 𝑢 = suc 𝑛)
20		eqcom 2744	. . . . . . . . . . . . . 14 ⊢ (𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢)
21	20	rexbii 3085	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
22	19, 21	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
23	12, 18, 22	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
24		sucexg 7753	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ V → suc 𝑛 ∈ V)
25	24	elv 3435	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑛 ∈ V
26	25	sucex 7754	. . . . . . . . . . . . . . . 16 ⊢ suc suc 𝑛 ∈ V
27	26	mptex 7172	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V)
29		fineqvnttrclselem1 35284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ ω)
30	29	elexd 3454	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
31	30	ralrimivw 3134	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
32		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})
33	32	fnmpt 6633	. . . . . . . . . . . . . . . . 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 7817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
37	12, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ On)
38		eloni 6328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → Ord 𝑢)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → Ord 𝑢)
40	39	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord 𝑢)
41		ordeq 6325	. . . . . . . . . . . . . . . . . . . 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 7780	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∅ ∈ suc suc 𝑛)
46		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → 𝑢 ∈ (ω ∖ 1o))
47		oveq1 7368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = ∅ → (𝑣 +o 𝑑) = (∅ +o 𝑑))
48	47	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∅ → ((𝑣 +o 𝑑) = 𝑢 ↔ (∅ +o 𝑑) = 𝑢))
49	48	rabbidv 3397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∅ → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
50	49	unieqd 4864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = ∅ → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
51		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∅ ∈ suc suc 𝑛)
52		fineqvnttrclselem1 35284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
53	52	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
54	32, 50, 51, 53	fvmptd3 6966	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
55		oa0r 8467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 ∈ On → (∅ +o 𝑑) = 𝑑)
56	55	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ On → ((∅ +o 𝑑) = 𝑢 ↔ 𝑑 = 𝑢))
57	56	rabbiia 3394	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = 𝑢}
58		rabsn 4666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ 𝑑 = 𝑢} = {𝑢})
59	57, 58	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑢})
60	59	unieqd 4864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = ∪ {𝑢})
61		unisnv 4871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ {𝑢} = 𝑢
62	60, 61	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . 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 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
66	45, 46, 65	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
67		oveq1 7368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = suc 𝑛 → (𝑣 +o 𝑑) = (suc 𝑛 +o 𝑑))
68	67	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = suc 𝑛 → ((𝑣 +o 𝑑) = 𝑢 ↔ (suc 𝑛 +o 𝑑) = 𝑢))
69	68	rabbidv 3397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = suc 𝑛 → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
70	69	unieqd 4864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = suc 𝑛 → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
71	25	sucid 6402	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
72	71	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → suc 𝑛 ∈ suc suc 𝑛)
73		fineqvnttrclselem1 35284	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} ∈ ω)
74	32, 70, 72, 73	fvmptd3 6966	. . . . . . . . . . . . . . . . . 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 7368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 = 𝑢 → (suc 𝑛 +o 𝑑) = (𝑢 +o 𝑑))
77	76	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑛 = 𝑢 → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
78	77	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
79		oa0 8445	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ On → (𝑢 +o ∅) = 𝑢)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑢 +o ∅) = 𝑢)
81		oveq2 7369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ∅ → (𝑢 +o 𝑑) = (𝑢 +o ∅))
82	81	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = ∅ → ((𝑢 +o 𝑑) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
83	80, 82	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ → (𝑢 +o 𝑑) = 𝑢))
84		oveq2 7369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑑 → (𝑢 +o 𝑠) = (𝑢 +o 𝑑))
85	84	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑑 → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
86		oveq2 7369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = ∅ → (𝑢 +o 𝑠) = (𝑢 +o ∅))
87	86	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = ∅ → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
88		ssid 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑢 ⊆ 𝑢
89		oawordeu 8484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6373	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3683	. . . . . . . . . . . . . . . . . . . . . . . . 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 3396	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = ∅})
104	103	unieqd 4864	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ 𝑑 = ∅})
105		rabsn 4666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ∈ On → {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅})
106	94, 105	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅}
107	106	unieqi 4863	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∪ {∅}
108		0ex 5243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ V
109	108	unisn 4870	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {∅} = ∅
110	107, 109	eqtri 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∅
111	104, 110	eqtrdi 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
112	37, 111	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
113	75, 112	eqtrd 2772	. . . . . . . . . . . . . . . 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 3434	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
116	115	sucid 6402	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ suc 𝑛
117		eleq2 2826	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑛 = 𝑢 → (𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢))
118	116, 117	mpbii 233	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢)
119		fineqvnttrclse.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
120		oveq2 7369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑒 → (𝑣 +o 𝑑) = (𝑣 +o 𝑒))
121	120	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑒 → ((𝑣 +o 𝑑) = 𝑢 ↔ (𝑣 +o 𝑒) = 𝑢))
122	121	cbvrabv 3400	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
123	122	unieqi 4863	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
124	123	mpteq2i 5182	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢})
125	119, 10, 124	fineqvnttrclselem3 35286	. . . . . . . . . . . . . . . 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 6584	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓 Fn suc suc 𝑛 ↔ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛))
129		fveq1 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘∅) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅))
130	129	eqeq1d 2739	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘∅) = 𝑢 ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢))
131		fveq1 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑛) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛))
132	131	eqeq1d 2739	. . . . . . . . . . . . . . . 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 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎))
135		fveq1 6834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
136	134, 135	breq12d 5099	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
137	136	ralbidv 3161	. . . . . . . . . . . . . . 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 3541	. . . . . . . . . . . . 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 3153	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → (∃𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
142	23, 141	mpd 15	. . . . . . . . . 10 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
143		brttrcl2 9629	. . . . . . . . . 10 ⊢ (𝑢t++𝑅∅ ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
144	142, 143	sylibr 234	. . . . . . . . 9 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++𝑅∅)
145	119	relopabiv 5770	. . . . . . . . . . . 12 ⊢ Rel 𝑅
146	119	dmeqi 5854	. . . . . . . . . . . . 13 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
147		dmopabss 5868	. . . . . . . . . . . . 13 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} ⊆ 𝐴
148	146, 147	eqsstri 3969	. . . . . . . . . . . 12 ⊢ dom 𝑅 ⊆ 𝐴
149		relssres 5982	. . . . . . . . . . . 12 ⊢ ((Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴) → (𝑅 ↾ 𝐴) = 𝑅)
150	145, 148, 149	mp2an 693	. . . . . . . . . . 11 ⊢ (𝑅 ↾ 𝐴) = 𝑅
151		ttrcleq 9624	. . . . . . . . . . 11 ⊢ ((𝑅 ↾ 𝐴) = 𝑅 → t++(𝑅 ↾ 𝐴) = t++𝑅)
152	150, 151	ax-mp 5	. . . . . . . . . 10 ⊢ t++(𝑅 ↾ 𝐴) = t++𝑅
153	152	breqi 5092	. . . . . . . . 9 ⊢ (𝑢t++(𝑅 ↾ 𝐴)∅ ↔ 𝑢t++𝑅∅)
154	144, 153	sylibr 234	. . . . . . . 8 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++(𝑅 ↾ 𝐴)∅)
155	154	rgen 3054	. . . . . . 7 ⊢ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅
156		ssrab 4012	. . . . . . 7 ⊢ ((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ↔ ((ω ∖ 1o) ⊆ 𝐴 ∧ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅))
157	11, 155, 156	mpbir2an 712	. . . . . 6 ⊢ (ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅}
158		ssexg 5261	. . . . . 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 7834	. . . . . . 7 ⊢ ∅ ∈ ω
162	161, 10	eleqtrri 2836	. . . . . 6 ⊢ ∅ ∈ 𝐴
163		breq2 5090	. . . . . . . . 9 ⊢ (𝑡 = ∅ → (𝑢t++(𝑅 ↾ 𝐴)𝑡 ↔ 𝑢t++(𝑅 ↾ 𝐴)∅))
164	163	rabbidv 3397	. . . . . . . 8 ⊢ (𝑡 = ∅ → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} = {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅})
165	164	eleq1d 2822	. . . . . . 7 ⊢ (𝑡 = ∅ → ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V ↔ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
166	165	rspcv 3561	. . . . . 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 5579	. . 3 ⊢ (t++(𝑅 ↾ 𝐴) Se 𝐴 ↔ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
171	169, 170	sylnibr 329	. 2 ⊢ (Fin = V → ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)
172		vex 3434	. . . . . . . . . 10 ⊢ 𝑤 ∈ V
173		vex 3434	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
174		eleq1w 2820	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
175		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦))
176	174, 175	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦)))
177		suceq 6386	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
178	177	eqeq2d 2748	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧))
179	178	anbi2d 631	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧)))
180	172, 173, 176, 179, 119	brab 5492	. . . . . . . . 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 3393	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} = {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧}
188	173	sucex 7754	. . . . . . . 8 ⊢ suc 𝑧 ∈ V
189	188	eueqi 3656	. . . . . . 7 ⊢ ∃!𝑤 𝑤 = suc 𝑧
190		euabex 5409	. . . . . . 7 ⊢ (∃!𝑤 𝑤 = suc 𝑧 → {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V)
191	189, 190	ax-mp 5	. . . . . 6 ⊢ {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V
192		rabssab 4026	. . . . . 6 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ⊆ {𝑤 ∣ 𝑤 = suc 𝑧}
193	191, 192	ssexi 5260	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ∈ V
194	187, 193	eqeltri 2833	. . . 4 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
195	194	rgenw 3056	. . 3 ⊢ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
196		df-se 5579	. . 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 2569  {cab 2715   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  ∃!wreu 3341  {crab 3390  Vcvv 3430   ∖ cdif 3887   ⊆ wss 3890  ∅c0 4274  {csn 4568  ∪ cuni 4851   class class class wbr 5086  {copab 5148   ↦ cmpt 5167   Se wse 5576  dom cdm 5625   ↾ cres 5627  Rel wrel 5630  Ord word 6317  Oncon0 6318  suc csuc 6320   Fn wfn 6488  ‘cfv 6493  (class class class)co 7361  ωcom 7811  1_oc1o 8392   +_o coa 8396  Fincfn 8887  t++cttrcl 9622

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 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-oadd 8403  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-ttrcl 9623

This theorem is referenced by: (None)