Metamath Proof Explorer

Theorem mh-inf3f1

Description: A variant of inf3 . If F is a one-to-one function from A into itself, and there exists an element B not in its range, then ` ( rec ( F , B ) |`_om ) is an infinite sequence of distinct elements from A . If A is a set, we can use this theorem to prove _om e. _V via f1dmex . (Contributed by Matthew House, 13-Apr-2026)

Ref Expression
Hypotheses mh-inf3f1.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐴 )
mh-inf3f1.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∖ ran 𝐹 ) )
Assertion mh-inf3f1 ( 𝜑 → ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 mh-inf3f1.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐴 )
2 mh-inf3f1.2 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 ∖ ran 𝐹 ) )
3 frfnom ⊢ ( rec ( 𝐹 , 𝐵 ) ↾ ω ) Fn ω
4 3 a1i ⊢ ( 𝜑 → ( rec ( 𝐹 , 𝐵 ) ↾ ω ) Fn ω )
5 fveq2 ⊢ ( 𝑥 = ∅ → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) )
6 5 eleq1d ⊢ ( 𝑥 = ∅ → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) ∈ 𝐴 ) )
7 fveq2 ⊢ ( 𝑥 = 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) )
8 7 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 ) )
9 fveq2 ⊢ ( 𝑥 = suc 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) )
10 9 eleq1d ⊢ ( 𝑥 = suc 𝑤 → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐴 ) )
11 2 eldifad ⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
12 fr0g ⊢ ( 𝐵 ∈ 𝐴 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) = 𝐵 )
13 11 12 syl ⊢ ( 𝜑 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) = 𝐵 )
14 13 11 eqeltrd ⊢ ( 𝜑 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) ∈ 𝐴 )
15 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
16 1 15 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐴 )
17 16 ffvelcdmda ⊢ ( ( 𝜑 ∧ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 ) → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) ∈ 𝐴 )
18 frsuc ⊢ ( 𝑤 ∈ ω → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
19 18 eleq1d ⊢ ( 𝑤 ∈ ω → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐴 ↔ ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) ∈ 𝐴 ) )
20 17 19 imbitrrid ⊢ ( 𝑤 ∈ ω → ( ( 𝜑 ∧ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐴 ) )
21 20 expd ⊢ ( 𝑤 ∈ ω → ( 𝜑 → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ∈ 𝐴 ) ) )
22 6 8 10 14 21 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝜑 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ) )
23 22 com12 ⊢ ( 𝜑 → ( 𝑥 ∈ ω → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ) )
24 23 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 )
25 ffnfv ⊢ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω ⟶ 𝐴 ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) Fn ω ∧ ∀ 𝑥 ∈ ω ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ∈ 𝐴 ) )
26 4 24 25 sylanbrc ⊢ ( 𝜑 → ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω ⟶ 𝐴 )
27 nnord ⊢ ( 𝑧 ∈ ω → Ord 𝑧 )
28 nnord ⊢ ( 𝑤 ∈ ω → Ord 𝑤 )
29 ordtri3 ⊢ ( ( Ord 𝑧 ∧ Ord 𝑤 ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
30 27 28 29 syl2an ⊢ ( ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ) )
32 31 necon2abid ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) ↔ 𝑧 ≠ 𝑤 ) )
33 vex ⊢ 𝑧 ∈ V
34 vex ⊢ 𝑤 ∈ V
35 simpl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
36 35 eleq1d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ ω ↔ 𝑧 ∈ ω ) )
37 simpr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
38 37 eleq1d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ ω ↔ 𝑤 ∈ ω ) )
39 36 38 anbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ↔ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) )
40 39 anbi2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ↔ ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) ) )
41 elequ12 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤 ) )
42 35 fveq2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) )
43 37 fveq2d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) )
44 42 43 neeq12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
45 41 44 imbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) ) )
46 40 45 imbi12d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥 ∈ 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑧 ∈ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) ) ) )
47 nnaordex2 ⊢ ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝑥 ∈ 𝑦 ↔ ∃ 𝑧 ∈ ω ( 𝑥 +o suc 𝑧 ) = 𝑦 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥 ∈ 𝑦 ↔ ∃ 𝑧 ∈ ω ( 𝑥 +o suc 𝑧 ) = 𝑦 ) )
49 oveq2 ⊢ ( 𝑥 = ∅ → ( suc 𝑧 +o 𝑥 ) = ( suc 𝑧 +o ∅ ) )
50 49 fveq2d ⊢ ( 𝑥 = ∅ → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o ∅ ) ) )
51 5 50 neeq12d ⊢ ( 𝑥 = ∅ → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o ∅ ) ) ) )
52 oveq2 ⊢ ( 𝑥 = 𝑤 → ( suc 𝑧 +o 𝑥 ) = ( suc 𝑧 +o 𝑤 ) )
53 52 fveq2d ⊢ ( 𝑥 = 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) )
54 7 53 neeq12d ⊢ ( 𝑥 = 𝑤 → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
55 oveq2 ⊢ ( 𝑥 = suc 𝑤 → ( suc 𝑧 +o 𝑥 ) = ( suc 𝑧 +o suc 𝑤 ) )
56 55 fveq2d ⊢ ( 𝑥 = suc 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) )
57 9 56 neeq12d ⊢ ( 𝑥 = suc 𝑤 → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) ) )
58 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → 𝐹 Fn 𝐴 )
60 26 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ∈ 𝐴 )
61 59 60 fnfvelrnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ∈ ran 𝐹 )
62 2 eldifbd ⊢ ( 𝜑 → ¬ 𝐵 ∈ ran 𝐹 )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ¬ 𝐵 ∈ ran 𝐹 )
64 nelne2 ⊢ ( ( ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹 ) → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ≠ 𝐵 )
65 61 63 64 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ≠ 𝐵 )
66 65 necomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → 𝐵 ≠ ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
67 13 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) = 𝐵 )
68 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → suc 𝑧 ∈ ω )
70 nna0 ⊢ ( suc 𝑧 ∈ ω → ( suc 𝑧 +o ∅ ) = suc 𝑧 )
71 69 70 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( suc 𝑧 +o ∅ ) = suc 𝑧 )
72 71 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o ∅ ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑧 ) )
73 frsuc ⊢ ( 𝑧 ∈ ω → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑧 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑧 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
75 72 74 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o ∅ ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
76 66 67 75 3netr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ∅ ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o ∅ ) ) )
77 18 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
78 nnasuc ⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) → ( suc 𝑧 +o suc 𝑤 ) = suc ( suc 𝑧 +o 𝑤 ) )
79 69 78 sylan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( suc 𝑧 +o suc 𝑤 ) = suc ( suc 𝑧 +o 𝑤 ) )
80 79 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc ( suc 𝑧 +o 𝑤 ) ) )
81 nnacl ⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) → ( suc 𝑧 +o 𝑤 ) ∈ ω )
82 69 81 sylan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( suc 𝑧 +o 𝑤 ) ∈ ω )
83 frsuc ⊢ ( ( suc 𝑧 +o 𝑤 ) ∈ ω → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc ( suc 𝑧 +o 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
84 82 83 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc ( suc 𝑧 +o 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
85 80 84 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
86 77 85 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) ↔ ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) ) )
87 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → 𝐹 : 𝐴 –1-1→ 𝐴 )
88 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω ⟶ 𝐴 )
89 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → 𝑤 ∈ ω )
90 88 89 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 )
91 88 82 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ∈ 𝐴 )
92 f1veqaeq ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐴 ∧ ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
93 87 90 91 92 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) = ( 𝐹 ‘ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
94 86 93 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) ) )
95 94 necon3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑤 ∈ ω ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) ) )
96 95 expcom ⊢ ( 𝑤 ∈ ω → ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑤 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ suc 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o suc 𝑤 ) ) ) ) )
97 51 54 57 76 96 finds2 ⊢ ( 𝑥 ∈ ω → ( ( 𝜑 ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) ) )
98 97 impcom ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ω ) ∧ 𝑥 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) )
99 98 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ 𝑧 ∈ ω ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) )
100 99 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) )
101 68 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → suc 𝑧 ∈ ω )
102 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → 𝑥 ∈ ω )
103 nnacom ⊢ ( ( suc 𝑧 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑧 +o 𝑥 ) = ( 𝑥 +o suc 𝑧 ) )
104 101 102 103 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( suc 𝑧 +o 𝑥 ) = ( 𝑥 +o suc 𝑧 ) )
105 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( 𝑥 +o suc 𝑧 ) = 𝑦 )
106 104 105 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( suc 𝑧 +o 𝑥 ) = 𝑦 )
107 106 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ ( suc 𝑧 +o 𝑥 ) ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) )
108 100 107 neeqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝑥 +o suc 𝑧 ) = 𝑦 ) ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) )
109 108 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( ∃ 𝑧 ∈ ω ( 𝑥 +o suc 𝑧 ) = 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) )
110 109 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( ∃ 𝑧 ∈ ω ( 𝑥 +o suc 𝑧 ) = 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) )
111 48 110 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥 ∈ 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) )
112 33 34 46 111 vtocl2 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑧 ∈ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
113 simpl ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑤 )
114 113 eleq1d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( 𝑥 ∈ ω ↔ 𝑤 ∈ ω ) )
115 simpr ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
116 115 eleq1d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( 𝑦 ∈ ω ↔ 𝑧 ∈ ω ) )
117 114 116 anbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ↔ ( 𝑤 ∈ ω ∧ 𝑧 ∈ ω ) ) )
118 117 anbi2d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) ↔ ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ 𝑧 ∈ ω ) ) ) )
119 elequ12 ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧 ) )
120 113 fveq2d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) )
121 115 fveq2d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) = ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) )
122 120 121 neeq12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
123 119 122 imbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( 𝑥 ∈ 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑧 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ) )
124 118 123 imbi12d ⊢ ( ( 𝑥 = 𝑤 ∧ 𝑦 = 𝑧 ) → ( ( ( 𝜑 ∧ ( 𝑥 ∈ ω ∧ 𝑦 ∈ ω ) ) → ( 𝑥 ∈ 𝑦 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑥 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑤 ∈ 𝑧 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) ) ) )
125 34 33 124 111 vtocl2 ⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ ω ∧ 𝑧 ∈ ω ) ) → ( 𝑤 ∈ 𝑧 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
126 125 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑤 ∈ 𝑧 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ) )
127 necom ⊢ ( ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) )
128 126 127 imbitrrdi ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑤 ∈ 𝑧 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
129 112 128 jaod ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( ( 𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧 ) → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
130 32 129 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ω ∧ 𝑤 ∈ ω ) ) → ( 𝑧 ≠ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
131 130 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ω ∀ 𝑤 ∈ ω ( 𝑧 ≠ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) )
132 dff14a ⊢ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω –1-1→ 𝐴 ↔ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω ⟶ 𝐴 ∧ ∀ 𝑧 ∈ ω ∀ 𝑤 ∈ ω ( 𝑧 ≠ 𝑤 → ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑧 ) ≠ ( ( rec ( 𝐹 , 𝐵 ) ↾ ω ) ‘ 𝑤 ) ) ) )
133 26 131 132 sylanbrc ⊢ ( 𝜑 → ( rec ( 𝐹 , 𝐵 ) ↾ ω ) : ω –1-1→ 𝐴 )