Metamath Proof Explorer

Theorem fineqvnttrclse

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

Ref Expression
Hypotheses fineqvnttrclse.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) }
fineqvnttrclse.2 ⊢ 𝐴 = ω
Assertion fineqvnttrclse ( Fin = V → ( 𝑅 Se 𝐴 ∧ ¬ t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fineqvnttrclse.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) }
2 fineqvnttrclse.2 ⊢ 𝐴 = ω
3 ominf ⊢ ¬ ω ∈ Fin
4 1onn ⊢ 1o ∈ ω
5 nnfi ⊢ ( 1o ∈ ω → 1o ∈ Fin )
6 4 5 ax-mp ⊢ 1o ∈ Fin
7 difinf ⊢ ( ( ¬ ω ∈ Fin ∧ 1o ∈ Fin ) → ¬ ( ω ∖ 1o ) ∈ Fin )
8 3 6 7 mp2an ⊢ ¬ ( ω ∖ 1o ) ∈ Fin
9 eleq2 ⊢ ( Fin = V → ( ( ω ∖ 1o ) ∈ Fin ↔ ( ω ∖ 1o ) ∈ V ) )
10 8 9 mtbii ⊢ ( Fin = V → ¬ ( ω ∖ 1o ) ∈ V )
11 difss ⊢ ( ω ∖ 1o ) ⊆ ω
12 11 2 sseqtrri ⊢ ( ω ∖ 1o ) ⊆ 𝐴
13 eldifi ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → 𝑢 ∈ ω )
14 eldifn ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ¬ 𝑢 ∈ 1o )
15 0lt1o ⊢ ∅ ∈ 1o
16 eleq1 ⊢ ( 𝑢 = ∅ → ( 𝑢 ∈ 1o ↔ ∅ ∈ 1o ) )
17 15 16 mpbiri ⊢ ( 𝑢 = ∅ → 𝑢 ∈ 1o )
18 17 necon3bi ⊢ ( ¬ 𝑢 ∈ 1o → 𝑢 ≠ ∅ )
19 14 18 syl ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → 𝑢 ≠ ∅ )
20 nnsuc ⊢ ( ( 𝑢 ∈ ω ∧ 𝑢 ≠ ∅ ) → ∃ 𝑛 ∈ ω 𝑢 = suc 𝑛 )
21 eqcom ⊢ ( 𝑢 = suc 𝑛 ↔ suc 𝑛 = 𝑢 )
22 21 rexbii ⊢ ( ∃ 𝑛 ∈ ω 𝑢 = suc 𝑛 ↔ ∃ 𝑛 ∈ ω suc 𝑛 = 𝑢 )
23 20 22 sylib ⊢ ( ( 𝑢 ∈ ω ∧ 𝑢 ≠ ∅ ) → ∃ 𝑛 ∈ ω suc 𝑛 = 𝑢 )
24 13 19 23 syl2anc ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∃ 𝑛 ∈ ω suc 𝑛 = 𝑢 )
25 sucexg ⊢ ( 𝑛 ∈ V → suc 𝑛 ∈ V )
26 25 elv ⊢ suc 𝑛 ∈ V
27 26 sucex ⊢ suc suc 𝑛 ∈ V
28 27 mptex ⊢ ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ∈ V
29 28 a1i ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ∈ V )
30 fineqvnttrclselem1 ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ∈ ω )
31 30 elexd ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ∈ V )
32 31 ralrimivw ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∀ 𝑣 ∈ suc suc 𝑛 ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ∈ V )
33 eqid ⊢ ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } )
34 33 fnmpt ⊢ ( ∀ 𝑣 ∈ suc suc 𝑛 ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ∈ V → ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) Fn suc suc 𝑛 )
35 32 34 syl ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) Fn suc suc 𝑛 )
36 35 adantr ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) Fn suc suc 𝑛 )
37 nnon ⊢ ( 𝑢 ∈ ω → 𝑢 ∈ On )
38 13 37 syl ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → 𝑢 ∈ On )
39 eloni ⊢ ( 𝑢 ∈ On → Ord 𝑢 )
40 38 39 syl ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → Ord 𝑢 )
41 40 adantr ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → Ord 𝑢 )
42 ordeq ⊢ ( suc 𝑛 = 𝑢 → ( Ord suc 𝑛 ↔ Ord 𝑢 ) )
43 42 adantl ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( Ord suc 𝑛 ↔ Ord 𝑢 ) )
44 41 43 mpbird ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → Ord suc 𝑛 )
45 0elsuc ⊢ ( Ord suc 𝑛 → ∅ ∈ suc suc 𝑛 )
46 44 45 syl ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ∅ ∈ suc suc 𝑛 )
47 simpl ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → 𝑢 ∈ ( ω ∖ 1o ) )
48 oveq1 ⊢ ( 𝑣 = ∅ → ( 𝑣 +o 𝑑 ) = ( ∅ +o 𝑑 ) )
49 48 eqeq1d ⊢ ( 𝑣 = ∅ → ( ( 𝑣 +o 𝑑 ) = 𝑢 ↔ ( ∅ +o 𝑑 ) = 𝑢 ) )
50 49 rabbidv ⊢ ( 𝑣 = ∅ → { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } )
51 50 unieqd ⊢ ( 𝑣 = ∅ → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } )
52 simpl ⊢ ( ( ∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ ( ω ∖ 1o ) ) → ∅ ∈ suc suc 𝑛 )
53 fineqvnttrclselem1 ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } ∈ ω )
54 53 adantl ⊢ ( ( ∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ ( ω ∖ 1o ) ) → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } ∈ ω )
55 33 51 52 54 fvmptd3 ⊢ ( ( ∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ ( ω ∖ 1o ) ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } )
56 oa0r ⊢ ( 𝑑 ∈ On → ( ∅ +o 𝑑 ) = 𝑑 )
57 56 eqeq1d ⊢ ( 𝑑 ∈ On → ( ( ∅ +o 𝑑 ) = 𝑢 ↔ 𝑑 = 𝑢 ) )
58 57 rabbiia ⊢ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = { 𝑑 ∈ On ∣ 𝑑 = 𝑢 }
59 rabsn ⊢ ( 𝑢 ∈ On → { 𝑑 ∈ On ∣ 𝑑 = 𝑢 } = { 𝑢 } )
60 58 59 eqtrid ⊢ ( 𝑢 ∈ On → { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = { 𝑢 } )
61 60 unieqd ⊢ ( 𝑢 ∈ On → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = ∪ { 𝑢 } )
62 unisnv ⊢ ∪ { 𝑢 } = 𝑢
63 61 62 eqtrdi ⊢ ( 𝑢 ∈ On → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = 𝑢 )
64 38 63 syl ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = 𝑢 )
65 64 adantl ⊢ ( ( ∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ ( ω ∖ 1o ) ) → ∪ { 𝑑 ∈ On ∣ ( ∅ +o 𝑑 ) = 𝑢 } = 𝑢 )
66 55 65 eqtrd ⊢ ( ( ∅ ∈ suc suc 𝑛 ∧ 𝑢 ∈ ( ω ∖ 1o ) ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = 𝑢 )
67 46 47 66 syl2anc ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = 𝑢 )
68 oveq1 ⊢ ( 𝑣 = suc 𝑛 → ( 𝑣 +o 𝑑 ) = ( suc 𝑛 +o 𝑑 ) )
69 68 eqeq1d ⊢ ( 𝑣 = suc 𝑛 → ( ( 𝑣 +o 𝑑 ) = 𝑢 ↔ ( suc 𝑛 +o 𝑑 ) = 𝑢 ) )
70 69 rabbidv ⊢ ( 𝑣 = suc 𝑛 → { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } )
71 70 unieqd ⊢ ( 𝑣 = suc 𝑛 → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } )
72 26 sucid ⊢ suc 𝑛 ∈ suc suc 𝑛
73 72 a1i ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → suc 𝑛 ∈ suc suc 𝑛 )
74 fineqvnttrclselem1 ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } ∈ ω )
75 33 71 73 74 fvmptd3 ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } )
76 75 adantr ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } )
77 oveq1 ⊢ ( suc 𝑛 = 𝑢 → ( suc 𝑛 +o 𝑑 ) = ( 𝑢 +o 𝑑 ) )
78 77 eqeq1d ⊢ ( suc 𝑛 = 𝑢 → ( ( suc 𝑛 +o 𝑑 ) = 𝑢 ↔ ( 𝑢 +o 𝑑 ) = 𝑢 ) )
79 78 ad2antlr ⊢ ( ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) ∧ 𝑑 ∈ On ) → ( ( suc 𝑛 +o 𝑑 ) = 𝑢 ↔ ( 𝑢 +o 𝑑 ) = 𝑢 ) )
80 oa0 ⊢ ( 𝑢 ∈ On → ( 𝑢 +o ∅ ) = 𝑢 )
81 80 adantr ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑢 +o ∅ ) = 𝑢 )
82 oveq2 ⊢ ( 𝑑 = ∅ → ( 𝑢 +o 𝑑 ) = ( 𝑢 +o ∅ ) )
83 82 eqeq1d ⊢ ( 𝑑 = ∅ → ( ( 𝑢 +o 𝑑 ) = 𝑢 ↔ ( 𝑢 +o ∅ ) = 𝑢 ) )
84 81 83 syl5ibrcom ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑑 = ∅ → ( 𝑢 +o 𝑑 ) = 𝑢 ) )
85 oveq2 ⊢ ( 𝑠 = 𝑑 → ( 𝑢 +o 𝑠 ) = ( 𝑢 +o 𝑑 ) )
86 85 eqeq1d ⊢ ( 𝑠 = 𝑑 → ( ( 𝑢 +o 𝑠 ) = 𝑢 ↔ ( 𝑢 +o 𝑑 ) = 𝑢 ) )
87 oveq2 ⊢ ( 𝑠 = ∅ → ( 𝑢 +o 𝑠 ) = ( 𝑢 +o ∅ ) )
88 87 eqeq1d ⊢ ( 𝑠 = ∅ → ( ( 𝑢 +o 𝑠 ) = 𝑢 ↔ ( 𝑢 +o ∅ ) = 𝑢 ) )
89 ssid ⊢ 𝑢 ⊆ 𝑢
90 oawordeu ⊢ ( ( ( 𝑢 ∈ On ∧ 𝑢 ∈ On ) ∧ 𝑢 ⊆ 𝑢 ) → ∃! 𝑠 ∈ On ( 𝑢 +o 𝑠 ) = 𝑢 )
91 89 90 mpan2 ⊢ ( ( 𝑢 ∈ On ∧ 𝑢 ∈ On ) → ∃! 𝑠 ∈ On ( 𝑢 +o 𝑠 ) = 𝑢 )
92 91 anidms ⊢ ( 𝑢 ∈ On → ∃! 𝑠 ∈ On ( 𝑢 +o 𝑠 ) = 𝑢 )
93 92 3ad2ant1 ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → ∃! 𝑠 ∈ On ( 𝑢 +o 𝑠 ) = 𝑢 )
94 simp2 ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → 𝑑 ∈ On )
95 0elon ⊢ ∅ ∈ On
96 95 a1i ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → ∅ ∈ On )
97 simp3 ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → ( 𝑢 +o 𝑑 ) = 𝑢 )
98 80 3ad2ant1 ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → ( 𝑢 +o ∅ ) = 𝑢 )
99 86 88 93 94 96 97 98 reu2eqd ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ∧ ( 𝑢 +o 𝑑 ) = 𝑢 ) → 𝑑 = ∅ )
100 99 3expia ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ) → ( ( 𝑢 +o 𝑑 ) = 𝑢 → 𝑑 = ∅ ) )
101 84 100 impbid ⊢ ( ( 𝑢 ∈ On ∧ 𝑑 ∈ On ) → ( 𝑑 = ∅ ↔ ( 𝑢 +o 𝑑 ) = 𝑢 ) )
102 101 adantlr ⊢ ( ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) ∧ 𝑑 ∈ On ) → ( 𝑑 = ∅ ↔ ( 𝑢 +o 𝑑 ) = 𝑢 ) )
103 79 102 bitr4d ⊢ ( ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) ∧ 𝑑 ∈ On ) → ( ( suc 𝑛 +o 𝑑 ) = 𝑢 ↔ 𝑑 = ∅ ) )
104 103 rabbidva ⊢ ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) → { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } = { 𝑑 ∈ On ∣ 𝑑 = ∅ } )
105 104 unieqd ⊢ ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } = ∪ { 𝑑 ∈ On ∣ 𝑑 = ∅ } )
106 rabsn ⊢ ( ∅ ∈ On → { 𝑑 ∈ On ∣ 𝑑 = ∅ } = { ∅ } )
107 95 106 ax-mp ⊢ { 𝑑 ∈ On ∣ 𝑑 = ∅ } = { ∅ }
108 107 unieqi ⊢ ∪ { 𝑑 ∈ On ∣ 𝑑 = ∅ } = ∪ { ∅ }
109 0ex ⊢ ∅ ∈ V
110 109 unisn ⊢ ∪ { ∅ } = ∅
111 108 110 eqtri ⊢ ∪ { 𝑑 ∈ On ∣ 𝑑 = ∅ } = ∅
112 105 111 eqtrdi ⊢ ( ( 𝑢 ∈ On ∧ suc 𝑛 = 𝑢 ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } = ∅ )
113 38 112 sylan ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑛 +o 𝑑 ) = 𝑢 } = ∅ )
114 76 113 eqtrd ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∅ )
115 67 114 jca ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ( ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = 𝑢 ∧ ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∅ ) )
116 vex ⊢ 𝑛 ∈ V
117 116 sucid ⊢ 𝑛 ∈ suc 𝑛
118 eleq2 ⊢ ( suc 𝑛 = 𝑢 → ( 𝑛 ∈ suc 𝑛 ↔ 𝑛 ∈ 𝑢 ) )
119 117 118 mpbii ⊢ ( suc 𝑛 = 𝑢 → 𝑛 ∈ 𝑢 )
120 oveq2 ⊢ ( 𝑑 = 𝑒 → ( 𝑣 +o 𝑑 ) = ( 𝑣 +o 𝑒 ) )
121 120 eqeq1d ⊢ ( 𝑑 = 𝑒 → ( ( 𝑣 +o 𝑑 ) = 𝑢 ↔ ( 𝑣 +o 𝑒 ) = 𝑢 ) )
122 121 cbvrabv ⊢ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = { 𝑒 ∈ On ∣ ( 𝑣 +o 𝑒 ) = 𝑢 }
123 122 unieqi ⊢ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } = ∪ { 𝑒 ∈ On ∣ ( 𝑣 +o 𝑒 ) = 𝑢 }
124 123 mpteq2i ⊢ ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑒 ∈ On ∣ ( 𝑣 +o 𝑒 ) = 𝑢 } )
125 1 2 124 fineqvnttrclselem3 ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ 𝑛 ∈ 𝑢 ) → ∀ 𝑎 ∈ suc 𝑛 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ 𝑎 ) 𝑅 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑎 ) )
126 119 125 sylan2 ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ∀ 𝑎 ∈ suc 𝑛 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ 𝑎 ) 𝑅 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑎 ) )
127 36 115 126 3jca ⊢ ( ( 𝑢 ∈ ( ω ∖ 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 ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( 𝑓 Fn suc suc 𝑛 ↔ ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) Fn suc suc 𝑛 ) )
129 fveq1 ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( 𝑓 ‘ ∅ ) = ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) )
130 129 eqeq1d ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( ( 𝑓 ‘ ∅ ) = 𝑢 ↔ ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = 𝑢 ) )
131 fveq1 ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( 𝑓 ‘ suc 𝑛 ) = ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) )
132 131 eqeq1d ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( ( 𝑓 ‘ suc 𝑛 ) = ∅ ↔ ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∅ ) )
133 130 132 anbi12d ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ↔ ( ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ ∅ ) = 𝑢 ∧ ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑛 ) = ∅ ) ) )
134 fveq1 ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( 𝑓 ‘ 𝑎 ) = ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ 𝑎 ) )
135 fveq1 ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( 𝑓 ‘ suc 𝑎 ) = ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑎 ) )
136 134 135 breq12d ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ 𝑎 ) 𝑅 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑎 ) ) )
137 136 ralbidv ⊢ ( 𝑓 = ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) → ( ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ↔ ∀ 𝑎 ∈ suc 𝑛 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ 𝑎 ) 𝑅 ( ( 𝑣 ∈ suc suc 𝑛 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝑢 } ) ‘ suc 𝑎 ) ) )
138 128 133 137 3anbi123d ⊢ ( 𝑓 = ( 𝑣 ∈ 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 29 127 138 spcedv ⊢ ( ( 𝑢 ∈ ( ω ∖ 1o ) ∧ suc 𝑛 = 𝑢 ) → ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
140 139 ex ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ( suc 𝑛 = 𝑢 → ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
141 140 reximdv ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ( ∃ 𝑛 ∈ ω suc 𝑛 = 𝑢 → ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) ) )
142 24 141 mpd ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
143 brttrcl2 ⊢ ( 𝑢 t++ 𝑅 ∅ ↔ ∃ 𝑛 ∈ ω ∃ 𝑓 ( 𝑓 Fn suc suc 𝑛 ∧ ( ( 𝑓 ‘ ∅ ) = 𝑢 ∧ ( 𝑓 ‘ suc 𝑛 ) = ∅ ) ∧ ∀ 𝑎 ∈ suc 𝑛 ( 𝑓 ‘ 𝑎 ) 𝑅 ( 𝑓 ‘ suc 𝑎 ) ) )
144 142 143 sylibr ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → 𝑢 t++ 𝑅 ∅ )
145 1 relopabiv ⊢ Rel 𝑅
146 1 dmeqi ⊢ dom 𝑅 = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) }
147 dmopabss ⊢ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) } ⊆ 𝐴
148 146 147 eqsstri ⊢ dom 𝑅 ⊆ 𝐴
149 relssres ⊢ ( ( Rel 𝑅 ∧ dom 𝑅 ⊆ 𝐴 ) → ( 𝑅 ↾ 𝐴 ) = 𝑅 )
150 145 148 149 mp2an ⊢ ( 𝑅 ↾ 𝐴 ) = 𝑅
151 ttrcleq ⊢ ( ( 𝑅 ↾ 𝐴 ) = 𝑅 → t++ ( 𝑅 ↾ 𝐴 ) = t++ 𝑅 )
152 150 151 ax-mp ⊢ t++ ( 𝑅 ↾ 𝐴 ) = t++ 𝑅
153 152 breqi ⊢ ( 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ ↔ 𝑢 t++ 𝑅 ∅ )
154 144 153 sylibr ⊢ ( 𝑢 ∈ ( ω ∖ 1o ) → 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ )
155 154 rgen ⊢ ∀ 𝑢 ∈ ( ω ∖ 1o ) 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅
156 ssrab ⊢ ( ( ω ∖ 1o ) ⊆ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ↔ ( ( ω ∖ 1o ) ⊆ 𝐴 ∧ ∀ 𝑢 ∈ ( ω ∖ 1o ) 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ ) )
157 12 155 156 mpbir2an ⊢ ( ω ∖ 1o ) ⊆ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ }
158 ssexg ⊢ ( ( ( ω ∖ 1o ) ⊆ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∧ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V ) → ( ω ∖ 1o ) ∈ V )
159 157 158 mpan ⊢ ( { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V → ( ω ∖ 1o ) ∈ V )
160 159 con3i ⊢ ( ¬ ( ω ∖ 1o ) ∈ V → ¬ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V )
161 peano1 ⊢ ∅ ∈ ω
162 161 2 eleqtrri ⊢ ∅ ∈ 𝐴
163 breq2 ⊢ ( 𝑡 = ∅ → ( 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 ↔ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ ) )
164 163 rabbidv ⊢ ( 𝑡 = ∅ → { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } = { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } )
165 164 eleq1d ⊢ ( 𝑡 = ∅ → ( { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V ↔ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V ) )
166 165 rspcv ⊢ ( ∅ ∈ 𝐴 → ( ∀ 𝑡 ∈ 𝐴 { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V → { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V ) )
167 162 166 ax-mp ⊢ ( ∀ 𝑡 ∈ 𝐴 { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V → { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V )
168 167 con3i ⊢ ( ¬ { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) ∅ } ∈ V → ¬ ∀ 𝑡 ∈ 𝐴 { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V )
169 10 160 168 3syl ⊢ ( Fin = V → ¬ ∀ 𝑡 ∈ 𝐴 { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V )
170 df-se ⊢ ( t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ↔ ∀ 𝑡 ∈ 𝐴 { 𝑢 ∈ 𝐴 ∣ 𝑢 t++ ( 𝑅 ↾ 𝐴 ) 𝑡 } ∈ V )
171 169 170 sylnibr ⊢ ( Fin = V → ¬ t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 )
172 vex ⊢ 𝑤 ∈ V
173 vex ⊢ 𝑧 ∈ V
174 eleq1w ⊢ ( 𝑥 = 𝑤 → ( 𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴 ) )
175 eqeq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 = suc 𝑦 ↔ 𝑤 = suc 𝑦 ) )
176 174 175 anbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦 ) ) )
177 suceq ⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 )
178 177 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑤 = suc 𝑦 ↔ 𝑤 = suc 𝑧 ) )
179 178 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑦 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) ) )
180 172 173 176 179 1 brab ⊢ ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) )
181 180 bilani ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) → ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) )
182 simpl ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) → 𝑤 ∈ 𝐴 )
183 180 biimpri ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) → 𝑤 𝑅 𝑧 )
184 182 183 jca ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) → ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) )
185 181 184 impbii ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑤 𝑅 𝑧 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑤 = suc 𝑧 ) )
186 185 rabbia2 ⊢ { 𝑤 ∈ 𝐴 ∣ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧 }
187 173 sucex ⊢ suc 𝑧 ∈ V
188 187 eueqi ⊢ ∃! 𝑤 𝑤 = suc 𝑧
189 euabex ⊢ ( ∃! 𝑤 𝑤 = suc 𝑧 → { 𝑤 ∣ 𝑤 = suc 𝑧 } ∈ V )
190 188 189 ax-mp ⊢ { 𝑤 ∣ 𝑤 = suc 𝑧 } ∈ V
191 rabssab ⊢ { 𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧 } ⊆ { 𝑤 ∣ 𝑤 = suc 𝑧 }
192 190 191 ssexi ⊢ { 𝑤 ∈ 𝐴 ∣ 𝑤 = suc 𝑧 } ∈ V
193 186 192 eqeltri ⊢ { 𝑤 ∈ 𝐴 ∣ 𝑤 𝑅 𝑧 } ∈ V
194 193 rgenw ⊢ ∀ 𝑧 ∈ 𝐴 { 𝑤 ∈ 𝐴 ∣ 𝑤 𝑅 𝑧 } ∈ V
195 df-se ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 { 𝑤 ∈ 𝐴 ∣ 𝑤 𝑅 𝑧 } ∈ V )
196 194 195 mpbir ⊢ 𝑅 Se 𝐴
197 171 196 jctil ⊢ ( Fin = V → ( 𝑅 Se 𝐴 ∧ ¬ t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ) )