Theorem fineqvnttrclse 35420

Description: A counterexample demonstrating that ttrclse 9682 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 9208	. . . . . 6 ⊢ ¬ ω ∈ Fin
2		1onn 8610	. . . . . . 7 ⊢ 1o ∈ ω
3		nnfi 9136	. . . . . . 7 ⊢ (1o ∈ ω → 1o ∈ Fin)
4	2, 3	ax-mp 5	. . . . . 6 ⊢ 1o ∈ Fin
5		difinf 9255	. . . . . 6 ⊢ ((¬ ω ∈ Fin ∧ 1o ∈ Fin) → ¬ (ω ∖ 1o) ∈ Fin)
6	1, 4, 5	mp2an 702	. . . . 5 ⊢ ¬ (ω ∖ 1o) ∈ Fin
7		eleq2 2851	. . . . 5 ⊢ (Fin = V → ((ω ∖ 1o) ∈ Fin ↔ (ω ∖ 1o) ∈ V))
8	6, 7	mtbii 328	. . . 4 ⊢ (Fin = V → ¬ (ω ∖ 1o) ∈ V)
9		difss 4089	. . . . . . . 8 ⊢ (ω ∖ 1o) ⊆ ω
10		fineqvnttrclse.2	. . . . . . . 8 ⊢ 𝐴 = ω
11	9, 10	sseqtrri 3985	. . . . . . 7 ⊢ (ω ∖ 1o) ⊆ 𝐴
12		eldifi 4084	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ ω)
13		eldifn 4085	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ω ∖ 1o) → ¬ 𝑢 ∈ 1o)
14		0lt1o 8473	. . . . . . . . . . . . . . 15 ⊢ ∅ ∈ 1o
15		eleq1 2850	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ∅ → (𝑢 ∈ 1o ↔ ∅ ∈ 1o))
16	14, 15	mpbiri 260	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ∅ → 𝑢 ∈ 1o)
17	16	necon3bi 2983	. . . . . . . . . . . . 13 ⊢ (¬ 𝑢 ∈ 1o → 𝑢 ≠ ∅)
18	13, 17	syl 17	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ≠ ∅)
19		nnsuc 7864	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω 𝑢 = suc 𝑛)
20		eqcom 2769	. . . . . . . . . . . . . 14 ⊢ (𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢)
21	20	rexbii 3109	. . . . . . . . . . . . 13 ⊢ (∃𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
22	19, 21	sylib 220	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ω ∧ 𝑢 ≠ ∅) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
23	12, 18, 22	syl2anc 593	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω suc 𝑛 = 𝑢)
24		sucexg 7788	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ V → suc 𝑛 ∈ V)
25	24	elv 3459	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑛 ∈ V
26	25	sucex 7789	. . . . . . . . . . . . . . . 16 ⊢ suc suc 𝑛 ∈ V
27	26	mptex 7207	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V
28	27	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) ∈ V)
29		fineqvnttrclselem1 35417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ ω)
30	29	elexd 3477	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
31	30	ralrimivw 3158	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∀𝑣 ∈ suc suc 𝑛∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} ∈ V)
32		eqid 2762	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})
33	32	fnmpt 6661	. . . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛)
36		nnon 7852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ω → 𝑢 ∈ On)
37	12, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢 ∈ On)
38		eloni 6356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → Ord 𝑢)
39	37, 38	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → Ord 𝑢)
40	39	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord 𝑢)
41		ordeq 6353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (suc 𝑛 = 𝑢 → (Ord suc 𝑛 ↔ Ord 𝑢))
42	41	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (Ord suc 𝑛 ↔ Ord 𝑢))
43	40, 42	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → Ord suc 𝑛)
44		0elsuc 7815	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord suc 𝑛 → ∅ ∈ suc suc 𝑛)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∅ ∈ suc suc 𝑛)
46		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → 𝑢 ∈ (ω ∖ 1o))
47		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = ∅ → (𝑣 +o 𝑑) = (∅ +o 𝑑))
48	47	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = ∅ → ((𝑣 +o 𝑑) = 𝑢 ↔ (∅ +o 𝑑) = 𝑢))
49	48	rabbidv 3421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = ∅ → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
50	49	unieqd 4878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = ∅ → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
51		simpl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∅ ∈ suc suc 𝑛)
52		fineqvnttrclselem1 35417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
53	52	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} ∈ ω)
54	32, 50, 51, 53	fvmptd3 6999	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢})
55		oa0r 8507	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 ∈ On → (∅ +o 𝑑) = 𝑑)
56	55	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 ∈ On → ((∅ +o 𝑑) = 𝑢 ↔ 𝑑 = 𝑢))
57	56	rabbiia 3418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = 𝑢}
58		rabsn 4680	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ 𝑑 = 𝑢} = {𝑢})
59	57, 58	eqtrid 2809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ On → {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = {𝑢})
60	59	unieqd 4878	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = ∪ {𝑢})
61		unisnv 4885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ {𝑢} = 𝑢
62	60, 61	eqtrdi 2813	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ On → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
63	37, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
64	63	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ∪ {𝑑 ∈ On ∣ (∅ +o 𝑑) = 𝑢} = 𝑢)
65	54, 64	eqtrd 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ (ω ∖ 1o)) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
66	45, 46, 65	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢)
67		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = suc 𝑛 → (𝑣 +o 𝑑) = (suc 𝑛 +o 𝑑))
68	67	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = suc 𝑛 → ((𝑣 +o 𝑑) = 𝑢 ↔ (suc 𝑛 +o 𝑑) = 𝑢))
69	68	rabbidv 3421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = suc 𝑛 → {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
70	69	unieqd 4878	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑣 = suc 𝑛 → ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
71	25	sucid 6430	. . . . . . . . . . . . . . . . . . . 20 ⊢ suc 𝑛 ∈ suc suc 𝑛
72	71	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → suc 𝑛 ∈ suc suc 𝑛)
73		fineqvnttrclselem1 35417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} ∈ ω)
74	32, 70, 72, 73	fvmptd3 6999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (ω ∖ 1o) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
75	74	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢})
76		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (suc 𝑛 = 𝑢 → (suc 𝑛 +o 𝑑) = (𝑢 +o 𝑑))
77	76	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (suc 𝑛 = 𝑢 → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
78	77	ad2antlr 737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
79		oa0 8485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑢 ∈ On → (𝑢 +o ∅) = 𝑢)
80	79	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑢 +o ∅) = 𝑢)
81		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ∅ → (𝑢 +o 𝑑) = (𝑢 +o ∅))
82	81	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = ∅ → ((𝑢 +o 𝑑) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
83	80, 82	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ → (𝑢 +o 𝑑) = 𝑢))
84		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = 𝑑 → (𝑢 +o 𝑠) = (𝑢 +o 𝑑))
85	84	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑑 → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o 𝑑) = 𝑢))
86		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = ∅ → (𝑢 +o 𝑠) = (𝑢 +o ∅))
87	86	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = ∅ → ((𝑢 +o 𝑠) = 𝑢 ↔ (𝑢 +o ∅) = 𝑢))
88		ssid 3958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 𝑢 ⊆ 𝑢
89		oawordeu 8524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ On ∧ 𝑢 ∈ On) ∧ 𝑢 ⊆ 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
90	88, 89	mpan2 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑢 ∈ On ∧ 𝑢 ∈ On) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
91	90	anidms 574	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ On → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
92	91	3ad2ant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∃!𝑠 ∈ On (𝑢 +o 𝑠) = 𝑢)
93		simp2 1150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 ∈ On)
94		0elon 6401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ On
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → ∅ ∈ On)
96		simp3 1151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o 𝑑) = 𝑢)
97	79	3ad2ant1 1146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → (𝑢 +o ∅) = 𝑢)
98	85, 87, 92, 93, 95, 96, 97	reu2eqd 3699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On ∧ (𝑢 +o 𝑑) = 𝑢) → 𝑑 = ∅)
99	98	3expia 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → ((𝑢 +o 𝑑) = 𝑢 → 𝑑 = ∅))
100	83, 99	impbid 214	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ On ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
101	100	adantlr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → (𝑑 = ∅ ↔ (𝑢 +o 𝑑) = 𝑢))
102	78, 101	bitr4d 284	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) ∧ 𝑑 ∈ On) → ((suc 𝑛 +o 𝑑) = 𝑢 ↔ 𝑑 = ∅))
103	102	rabbidva 3420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = {𝑑 ∈ On ∣ 𝑑 = ∅})
104	103	unieqd 4878	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∪ {𝑑 ∈ On ∣ 𝑑 = ∅})
105		rabsn 4680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ∈ On → {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅})
106	94, 105	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑑 ∈ On ∣ 𝑑 = ∅} = {∅}
107	106	unieqi 4877	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∪ {∅}
108		0ex 5257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ V
109	108	unisn 4884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ {∅} = ∅
110	107, 109	eqtri 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ ∪ {𝑑 ∈ On ∣ 𝑑 = ∅} = ∅
111	104, 110	eqtrdi 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ On ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
112	37, 111	sylan 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∪ {𝑑 ∈ On ∣ (suc 𝑛 +o 𝑑) = 𝑢} = ∅)
113	75, 112	eqtrd 2797	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)
114	66, 113	jca 519	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
115		vex 3458	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑛 ∈ V
116	115	sucid 6430	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ suc 𝑛
117		eleq2 2851	. . . . . . . . . . . . . . . . 17 ⊢ (suc 𝑛 = 𝑢 → (𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢))
118	116, 117	mpbii 235	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢)
119		fineqvnttrclse.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
120		oveq2 7404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑒 → (𝑣 +o 𝑑) = (𝑣 +o 𝑒))
121	120	eqeq1d 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑒 → ((𝑣 +o 𝑑) = 𝑢 ↔ (𝑣 +o 𝑒) = 𝑢))
122	121	cbvrabv 3424	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
123	122	unieqi 4877	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢} = ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢}
124	123	mpteq2i 5196	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑒 ∈ On ∣ (𝑣 +o 𝑒) = 𝑢})
125	119, 10, 124	fineqvnttrclselem3 35419	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ 𝑛 ∈ 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
126	118, 125	sylan2 602	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
127	35, 114, 126	3jca 1141	. . . . . . . . . . . . . 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 6612	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓 Fn suc suc 𝑛 ↔ (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) Fn suc suc 𝑛))
129		fveq1 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘∅) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅))
130	129	eqeq1d 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘∅) = 𝑢 ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢))
131		fveq1 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑛) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛))
132	131	eqeq1d 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘suc 𝑛) = ∅ ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅))
133	130, 132	anbi12d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ↔ (((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘∅) = 𝑢 ∧ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑛) = ∅)))
134		fveq1 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎))
135		fveq1 6866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (𝑓‘suc 𝑎) = ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎))
136	134, 135	breq12d 5113	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → ((𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
137	136	ralbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢}) → (∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎) ↔ ∀𝑎 ∈ suc 𝑛((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘𝑎)𝑅((𝑣 ∈ suc suc 𝑛 ↦ ∪ {𝑑 ∈ On ∣ (𝑣 +o 𝑑) = 𝑢})‘suc 𝑎)))
138	128, 133, 137	3anbi123d 1457	. . . . . . . . . . . . . 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 3557	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ (ω ∖ 1o) ∧ suc 𝑛 = 𝑢) → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
140	139	ex 416	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ (ω ∖ 1o) → (suc 𝑛 = 𝑢 → ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
141	140	reximdv 3177	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (ω ∖ 1o) → (∃𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎))))
142	23, 141	mpd 15	. . . . . . . . . 10 ⊢ (𝑢 ∈ (ω ∖ 1o) → ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
143		brttrcl2 9669	. . . . . . . . . 10 ⊢ (𝑢t++𝑅∅ ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝑢 ∧ (𝑓‘suc 𝑛) = ∅) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
144	142, 143	sylibr 236	. . . . . . . . 9 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++𝑅∅)
145	119	relopabiv 5793	. . . . . . . . . . . 12 ⊢ Rel 𝑅
146	119	dmeqi 5880	. . . . . . . . . . . . 13 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)}
147		dmopabss 5894	. . . . . . . . . . . . 13 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦)} ⊆ 𝐴
148	146, 147	eqsstri 3982	. . . . . . . . . . . 12 ⊢ dom 𝑅 ⊆ 𝐴
149		relssres 6008	. . . . . . . . . . . 12 ⊢ ((Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴) → (𝑅 ↾ 𝐴) = 𝑅)
150	145, 148, 149	mp2an 702	. . . . . . . . . . 11 ⊢ (𝑅 ↾ 𝐴) = 𝑅
151		ttrcleq 9664	. . . . . . . . . . 11 ⊢ ((𝑅 ↾ 𝐴) = 𝑅 → t++(𝑅 ↾ 𝐴) = t++𝑅)
152	150, 151	ax-mp 5	. . . . . . . . . 10 ⊢ t++(𝑅 ↾ 𝐴) = t++𝑅
153	152	breqi 5106	. . . . . . . . 9 ⊢ (𝑢t++(𝑅 ↾ 𝐴)∅ ↔ 𝑢t++𝑅∅)
154	144, 153	sylibr 236	. . . . . . . 8 ⊢ (𝑢 ∈ (ω ∖ 1o) → 𝑢t++(𝑅 ↾ 𝐴)∅)
155	154	rgen 3078	. . . . . . 7 ⊢ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅
156		ssrab 4024	. . . . . . 7 ⊢ ((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ↔ ((ω ∖ 1o) ⊆ 𝐴 ∧ ∀𝑢 ∈ (ω ∖ 1o)𝑢t++(𝑅 ↾ 𝐴)∅))
157	11, 155, 156	mpbir2an 721	. . . . . 6 ⊢ (ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅}
158		ssexg 5279	. . . . . 6 ⊢ (((ω ∖ 1o) ⊆ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∧ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V) → (ω ∖ 1o) ∈ V)
159	157, 158	mpan 700	. . . . 5 ⊢ ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V → (ω ∖ 1o) ∈ V)
160	159	con3i 154	. . . 4 ⊢ (¬ (ω ∖ 1o) ∈ V → ¬ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V)
161		peano1 7869	. . . . . . 7 ⊢ ∅ ∈ ω
162	161, 10	eleqtrri 2861	. . . . . 6 ⊢ ∅ ∈ 𝐴
163		breq2 5104	. . . . . . . . 9 ⊢ (𝑡 = ∅ → (𝑢t++(𝑅 ↾ 𝐴)𝑡 ↔ 𝑢t++(𝑅 ↾ 𝐴)∅))
164	163	rabbidv 3421	. . . . . . . 8 ⊢ (𝑡 = ∅ → {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} = {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅})
165	164	eleq1d 2847	. . . . . . 7 ⊢ (𝑡 = ∅ → ({𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V ↔ {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)∅} ∈ V))
166	165	rspcv 3577	. . . . . 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 5601	. . 3 ⊢ (t++(𝑅 ↾ 𝐴) Se 𝐴 ↔ ∀𝑡 ∈ 𝐴 {𝑢 ∈ 𝐴 ∣ 𝑢t++(𝑅 ↾ 𝐴)𝑡} ∈ V)
171	169, 170	sylnibr 331	. 2 ⊢ (Fin = V → ¬ t++(𝑅 ↾ 𝐴) Se 𝐴)
172		vex 3458	. . . . . . . . 9 ⊢ 𝑤 ∈ V
173		vex 3458	. . . . . . . . 9 ⊢ 𝑧 ∈ V
174		eleq1w 2845	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
175		eqeq1 2766	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦))
176	174, 175	anbi12d 641	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦)))
177		suceq 6414	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧)
178	177	eqeq2d 2773	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧))
179	178	anbi2d 639	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧)))
180	172, 173, 176, 179, 119	brab 5514	. . . . . . . 8 ⊢ (𝑤𝑅𝑧 ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
181	180	bilani 508	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
182		simpl 486	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤 ∈ 𝐴)
183	180	biimpri 230	. . . . . . . 8 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → 𝑤𝑅𝑧)
184	182, 183	jca 519	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧) → (𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧))
185	181, 184	impbii 211	. . . . . 6 ⊢ ((𝑤 ∈ 𝐴 ∧ 𝑤𝑅𝑧) ↔ (𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧))
186	185	rabbia2 3417	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} = {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧}
187	173	sucex 7789	. . . . . . . 8 ⊢ suc 𝑧 ∈ V
188	187	eueqi 3672	. . . . . . 7 ⊢ ∃!𝑤 𝑤 = suc 𝑧
189		euabex 5428	. . . . . . 7 ⊢ (∃!𝑤 𝑤 = suc 𝑧 → {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V)
190	188, 189	ax-mp 5	. . . . . 6 ⊢ {𝑤 ∣ 𝑤 = suc 𝑧} ∈ V
191		rabssab 4038	. . . . . 6 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ⊆ {𝑤 ∣ 𝑤 = suc 𝑧}
192	190, 191	ssexi 5278	. . . . 5 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧} ∈ V
193	186, 192	eqeltri 2858	. . . 4 ⊢ {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
194	193	rgenw 3080	. . 3 ⊢ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V
195		df-se 5601	. . 3 ⊢ (𝑅 Se 𝐴 ↔ ∀𝑧 ∈ 𝐴 {𝑤 ∈ 𝐴 ∣ 𝑤𝑅𝑧} ∈ V)
196	194, 195	mpbir 233	. 2 ⊢ 𝑅 Se 𝐴
197	171, 196	jctil 527	1 ⊢ (Fin = V → (𝑅 Se 𝐴 ∧ ¬ t++(𝑅 ↾ 𝐴) Se 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560  ∃wex 1799   ∈ wcel 2142  ∃!weu 2595  {cab 2740   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  ∃!wreu 3365  {crab 3414  Vcvv 3454   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  {csn 4582  ∪ cuni 4865   class class class wbr 5100  {copab 5162   ↦ cmpt 5181   Se wse 5598  dom cdm 5647   ↾ cres 5649  Rel wrel 5652  Ord word 6345  Oncon0 6346  suc csuc 6348   Fn wfn 6516  ‘cfv 6521  (class class class)co 7396  ωcom 7846  1_oc1o 8430   +_o coa 8434  Fincfn 8927  t++cttrcl 9662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-oadd 8441  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-ttrcl 9663

This theorem is referenced by: (None)