Theorem fineqvnttrclse 35280

Description: A counterexample demonstrating that ttrclse 9636 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 8568	. . . . . . 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 692	. . . . 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 4088	. . . . . . . 8 ⊢ (ω ∖ 1o) ⊆ ω
10		fineqvnttrclse.2	. . . . . . . 8 ⊢ 𝐴 = ω
11	9, 10	sseqtrri 3983	. . . . . . 7 ⊢ (ω ∖ 1o) ⊆ 𝐴
12		eldifi 4083	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ ω)
13		eldifn 4084	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ω ∖ 1o) → ¬ 𝑢 ∈ 1o)
14		0lt1o 8431	. . . . . . . . . . . . . . 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 7826	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω 𝑢 = suc 𝑛)
20		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ (𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢)
21	20	rexbii 3083	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
22	19, 21	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
23	12, 18, 22	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
24		sucexg 7750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ V → suc 𝑛 ∈ V)
25	24	elv 3445	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑛 ∈ V
26	25	sucex 7751	. . . . . . . . . . . . . . . 16 ⊢ suc suc 𝑛 ∈ V
27	26	mptex 7169	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V)
29		fineqvnttrclselem1 35277	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ ω)
30	29	elexd 3464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
31	30	ralrimivw 3132	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
32		eqid 2736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})
33	32	fnmpt 6632	. . . . . . . . . . . . . . . . 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 7814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
37	12, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ On)
38		eloni 6327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → Ord 𝑢)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → Ord 𝑢)
40	39	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord 𝑢)
41		ordeq 6324	. . . . . . . . . . . . . . . . . . . 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 7777	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∅ ∈ suc suc 𝑛)
46		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → 𝑢 ∈ (ω ∖ 1o))
47		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = ∅ → (𝑣 +o 𝑑) = (∅ +o 𝑑))
48	47	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∅ → ((𝑣 +o 𝑑) = 𝑢 ↔ (∅ +o 𝑑) = 𝑢))
49	48	rabbidv 3406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∅ → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
50	49	unieqd 4876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = ∅ → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
51		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∅ ∈ suc suc 𝑛)
52		fineqvnttrclselem1 35277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
53	52	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
54	32, 50, 51, 53	fvmptd3 6964	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
55		oa0r 8465	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 ∈ On → (∅ +o 𝑑) = 𝑑)
56	55	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ On → ((∅ +o 𝑑) = 𝑢 ↔ 𝑑 = 𝑢))
57	56	rabbiia 3403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = 𝑢}
58		rabsn 4678	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ 𝑑 = 𝑢} = {𝑢})
59	57, 58	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑢})
60	59	unieqd 4876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = ∪ {𝑢})
61		unisnv 4883	. . . . . . . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
67		oveq1 7365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = suc 𝑛 → (𝑣 +o 𝑑) = (suc 𝑛 +o 𝑑))
68	67	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = suc 𝑛 → ((𝑣 +o 𝑑) = 𝑢 ↔ (suc 𝑛 +o 𝑑) = 𝑢))
69	68	rabbidv 3406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = suc 𝑛 → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
70	69	unieqd 4876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = suc 𝑛 → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
71	25	sucid 6401	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
72	71	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → suc 𝑛 ∈ suc suc 𝑛)
73		fineqvnttrclselem1 35277	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} ∈ ω)
74	32, 70, 72, 73	fvmptd3 6964	. . . . . . . . . . . . . . . . . 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 7365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 = 𝑢 → (suc 𝑛 +o 𝑑) = (𝑢 +o 𝑑))
77	76	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑛 = 𝑢 → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
78	77	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
79		oa0 8443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ On → (𝑢 +o ∅) = 𝑢)
80	79	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑢 +o ∅) = 𝑢)
81		oveq2 7366	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ∅ → (𝑢 +o 𝑑) = (𝑢 +o ∅))
82	81	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = ∅ → ((𝑢 +o 𝑑) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
83	80, 82	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ → (𝑢 +o 𝑑) = 𝑢))
84		oveq2 7366	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑑 → (𝑢 +o 𝑠) = (𝑢 +o 𝑑))
85	84	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑑 → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
86		oveq2 7366	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = ∅ → (𝑢 +o 𝑠) = (𝑢 +o ∅))
87	86	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = ∅ → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
88		ssid 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑢 ⊆ 𝑢
89		oawordeu 8482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ On ∧ 𝑢 ∈ On) ∧ 𝑢 ⊆ 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
90	88, 89	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ On ∧ 𝑢 ∈ On) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
91	90	anidms 566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ On → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
92	91	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
93		simp2 1137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 ∈ On)
94		0elon 6372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ On
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∅ ∈ On)
96		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o 𝑑) = 𝑢)
97	79	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o ∅) = 𝑢)
98	85, 87, 92, 93, 95, 96, 97	reu2eqd 3694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 = ∅)
99	98	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → ((𝑢 +o 𝑑) = 𝑢 → 𝑑 = ∅))
100	83, 99	impbid 212	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
101	100	adantlr 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
102	78, 101	bitr4d 282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ 𝑑 = ∅))
103	102	rabbidva 3405	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = ∅})
104	103	unieqd 4876	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ 𝑑 = ∅})
105		rabsn 4678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ∈ On → {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅})
106	94, 105	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅}
107	106	unieqi 4875	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∪ {∅}
108		0ex 5252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ V
109	108	unisn 4882	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {∅} = ∅
110	107, 109	eqtri 2759	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∅
111	104, 110	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
112	37, 111	sylan 580	. . . . . . . . . . . . . . . . 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 3444	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
116	115	sucid 6401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ suc 𝑛
117		eleq2 2825	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑛 = 𝑢 → (𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢))
118	116, 117	mpbii 233	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢)
119		fineqvnttrclse.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
120		oveq2 7366	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑒 → (𝑣 +o 𝑑) = (𝑣 +o 𝑒))
121	120	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑒 → ((𝑣 +o 𝑑) = 𝑢 ↔ (𝑣 +o 𝑒) = 𝑢))
122	121	cbvrabv 3409	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
123	122	unieqi 4875	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
124	123	mpteq2i 5194	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢})
125	119, 10, 124	fineqvnttrclselem3 35279	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ 𝑛 ∈ 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
126	118, 125	sylan2 593	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
127	35, 114, 126	3jca 1128	. . . . . . . . . . . . . 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 6583	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓 Fn suc suc 𝑛 ↔ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛))
129		fveq1 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘∅) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅))
130	129	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘∅) = 𝑢 ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢))
131		fveq1 6833	. . . . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ↔ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)))
134		fveq1 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎))
135		fveq1 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
136	134, 135	breq12d 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
137	136	ralbidv 3159	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
138	128, 133, 137	3anbi123d 1438	. . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . 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 3151	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → (∃𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
142	23, 141	mpd 15	. . . . . . . . . 10 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
143		brttrcl2 9623	. . . . . . . . . 10 ⊢ (𝑢t++𝑅∅ ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
144	142, 143	sylibr 234	. . . . . . . . 9 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++𝑅∅)
145	119	relopabiv 5769	. . . . . . . . . . . 12 ⊢ Rel 𝑅
146	119	dmeqi 5853	. . . . . . . . . . . . 13 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
147		dmopabss 5867	. . . . . . . . . . . . 13 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} ⊆ 𝐴
148	146, 147	eqsstri 3980	. . . . . . . . . . . 12 ⊢ dom 𝑅 ⊆ 𝐴
149		relssres 5981	. . . . . . . . . . . 12 ⊢ ((Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴) → (𝑅 ↾ 𝐴) = 𝑅)
150	145, 148, 149	mp2an 692	. . . . . . . . . . 11 ⊢ (𝑅 ↾ 𝐴) = 𝑅
151		ttrcleq 9618	. . . . . . . . . . 11 ⊢ ((𝑅 ↾ 𝐴) = 𝑅 → t++(𝑅 ↾ 𝐴) = t++𝑅)
152	150, 151	ax-mp 5	. . . . . . . . . 10 ⊢ t++(𝑅 ↾ 𝐴) = t++𝑅
153	152	breqi 5104	. . . . . . . . 9 ⊢ (𝑢t++(𝑅 ↾ 𝐴)∅ ↔ 𝑢t++𝑅∅)
154	144, 153	sylibr 234	. . . . . . . 8 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++(𝑅 ↾ 𝐴)∅)
155	154	rgen 3053	. . . . . . 7 ⊢ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅
156		ssrab 4023	. . . . . . 7 ⊢ ((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ↔ ((ω ∖ 1o) ⊆ 𝐴 ∧ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅))
157	11, 155, 156	mpbir2an 711	. . . . . 6 ⊢ (ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅}
158		ssexg 5268	. . . . . 6 ⊢ (((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∧ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V) → (ω ∖ 1o) ∈ V)
159	157, 158	mpan 690	. . . . 5 ⊢ ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V → (ω ∖ 1o) ∈ V)
160	159	con3i 154	. . . 4 ⊢ (¬ (ω ∖ 1o) ∈ V → ¬ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V)
161		peano1 7831	. . . . . . 7 ⊢ ∅ ∈ ω
162	161, 10	eleqtrri 2835	. . . . . 6 ⊢ ∅ ∈ 𝐴
163		breq2 5102	. . . . . . . . 9 ⊢ (𝑡 = ∅ → (𝑢t++(𝑅 ↾ 𝐴)𝑡 ↔ 𝑢t++(𝑅 ↾ 𝐴)∅))
164	163	rabbidv 3406	. . . . . . . 8 ⊢ (𝑡 = ∅ → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} = {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅})
165	164	eleq1d 2821	. . . . . . 7 ⊢ (𝑡 = ∅ → ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V ↔ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
166	165	rspcv 3572	. . . . . 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 5578	. . 3 ⊢ (t++(𝑅 ↾ 𝐴) Se 𝐴 ↔ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
171	169, 170	sylnibr 329	. 2 ⊢ (Fin = V → ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)
172		vex 3444	. . . . . . . . . 10 ⊢ 𝑤 ∈ V
173		vex 3444	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
174		eleq1w 2819	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
175		eqeq1 2740	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦))
176	174, 175	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦)))
177		suceq 6385	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
178	177	eqeq2d 2747	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → (𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧))
179	178	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧)))
180	172, 173, 176, 179, 119	brab 5491	. . . . . . . . 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 3402	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} = {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧}
188	173	sucex 7751	. . . . . . . 8 ⊢ suc 𝑧 ∈ V
189	188	eueqi 3667	. . . . . . 7 ⊢ ∃!𝑤 𝑤 = suc 𝑧
190		euabex 5409	. . . . . . 7 ⊢ (∃!𝑤 𝑤 = suc 𝑧 → {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V)
191	189, 190	ax-mp 5	. . . . . 6 ⊢ {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V
192		rabssab 4037	. . . . . 6 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ⊆ {𝑤 ∣ 𝑤 = suc 𝑧}
193	191, 192	ssexi 5267	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ∈ V
194	187, 193	eqeltri 2832	. . . 4 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
195	194	rgenw 3055	. . 3 ⊢ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
196		df-se 5578	. . 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 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃!weu 2568  {cab 2714   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  ∃!wreu 3348  {crab 3399  Vcvv 3440   ∖ cdif 3898   ⊆ wss 3901  ∅c0 4285  {csn 4580  ∪ cuni 4863   class class class wbr 5098  {copab 5160   ↦ cmpt 5179   Se wse 5575  dom cdm 5624   ↾ cres 5626  Rel wrel 5629  Ord word 6316  Oncon0 6317  suc csuc 6319   Fn wfn 6487  ‘cfv 6492  (class class class)co 7358  ωcom 7808  1_oc1o 8390   +_o coa 8394  Fincfn 8883  t++cttrcl 9616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  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 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-oadd 8401  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-ttrcl 9617

This theorem is referenced by: (None)