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 
|- ( ph -> F : A -1-1-> A )
mh-inf3f1.2 
|- ( ph -> B e. ( A \ ran F ) )
Assertion mh-inf3f1 
|- ( ph -> ( rec ( F , B ) |` _om ) : _om -1-1-> A )

Proof

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