Metamath Proof Explorer

Theorem mh-inf3f1

Description: A variant of inf3 . If F is a one-to-one function from A into itself, and B is an element outside its range, then ` ( rec ( F , B ) |`_om ) is a one-to-one function yielding 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 fveq2 
 |-  ( x = (/) -> ( ( rec ( F , B ) |` _om ) ` x ) = ( ( rec ( F , B ) |` _om ) ` (/) ) )
4 3 eleq1d 
 |-  ( x = (/) -> ( ( ( rec ( F , B ) |` _om ) ` x ) e. A <-> ( ( rec ( F , B ) |` _om ) ` (/) ) e. A ) )
5 fveq2 
 |-  ( x = z -> ( ( rec ( F , B ) |` _om ) ` x ) = ( ( rec ( F , B ) |` _om ) ` z ) )
6 5 eleq1d 
 |-  ( x = z -> ( ( ( rec ( F , B ) |` _om ) ` x ) e. A <-> ( ( rec ( F , B ) |` _om ) ` z ) e. A ) )
7 fveq2 
 |-  ( x = suc z -> ( ( rec ( F , B ) |` _om ) ` x ) = ( ( rec ( F , B ) |` _om ) ` suc z ) )
8 7 eleq1d 
 |-  ( x = suc z -> ( ( ( rec ( F , B ) |` _om ) ` x ) e. A <-> ( ( rec ( F , B ) |` _om ) ` suc z ) e. A ) )
9 fr0g 
 |-  ( B e. ( A \ ran F ) -> ( ( rec ( F , B ) |` _om ) ` (/) ) = B )
10 2 9 syl 
 |-  ( ph -> ( ( rec ( F , B ) |` _om ) ` (/) ) = B )
11 10 2 eqeltrd 
 |-  ( ph -> ( ( rec ( F , B ) |` _om ) ` (/) ) e. ( A \ ran F ) )
12 11 eldifad 
 |-  ( ph -> ( ( rec ( F , B ) |` _om ) ` (/) ) e. A )
13 f1f 
 |-  ( F : A -1-1-> A -> F : A --> A )
14 1 13 syl 
 |-  ( ph -> F : A --> A )
15 14 ffvelcdmda 
 |-  ( ( ph /\ ( ( rec ( F , B ) |` _om ) ` z ) e. A ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) e. A )
16 frsuc 
 |-  ( z e. _om -> ( ( rec ( F , B ) |` _om ) ` suc z ) = ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) )
17 16 eleq1d 
 |-  ( z e. _om -> ( ( ( rec ( F , B ) |` _om ) ` suc z ) e. A <-> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) e. A ) )
18 15 17 imbitrrid 
 |-  ( z e. _om -> ( ( ph /\ ( ( rec ( F , B ) |` _om ) ` z ) e. A ) -> ( ( rec ( F , B ) |` _om ) ` suc z ) e. A ) )
19 18 expd 
 |-  ( z e. _om -> ( ph -> ( ( ( rec ( F , B ) |` _om ) ` z ) e. A -> ( ( rec ( F , B ) |` _om ) ` suc z ) e. A ) ) )
20 4 6 8 12 19 finds2 
 |-  ( x e. _om -> ( ph -> ( ( rec ( F , B ) |` _om ) ` x ) e. A ) )
21 20 com12 
 |-  ( ph -> ( x e. _om -> ( ( rec ( F , B ) |` _om ) ` x ) e. A ) )
22 21 ralrimiv 
 |-  ( ph -> A. x e. _om ( ( rec ( F , B ) |` _om ) ` x ) e. A )
23 frfnom 
 |-  ( rec ( F , B ) |` _om ) Fn _om
24 ffnfv 
 |-  ( ( rec ( F , B ) |` _om ) : _om --> A <-> ( ( rec ( F , B ) |` _om ) Fn _om /\ A. x e. _om ( ( rec ( F , B ) |` _om ) ` x ) e. A ) )
25 23 24 mpbiran 
 |-  ( ( rec ( F , B ) |` _om ) : _om --> A <-> A. x e. _om ( ( rec ( F , B ) |` _om ) ` x ) e. A )
26 22 25 sylibr 
 |-  ( ph -> ( rec ( F , B ) |` _om ) : _om --> A )
27 3 neeq1d 
 |-  ( x = (/) -> ( ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> ( ( rec ( F , B ) |` _om ) ` (/) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
28 27 raleqbi1dv 
 |-  ( x = (/) -> ( A. y e. x ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> A. y e. (/) ( ( rec ( F , B ) |` _om ) ` (/) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
29 5 neeq1d 
 |-  ( x = z -> ( ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
30 29 raleqbi1dv 
 |-  ( x = z -> ( A. y e. x ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
31 7 neeq1d 
 |-  ( x = suc z -> ( ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
32 31 raleqbi1dv 
 |-  ( x = suc z -> ( A. y e. x ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> A. y e. suc z ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
33 ral0 
 |-  A. y e. (/) ( ( rec ( F , B ) |` _om ) ` (/) ) =/= ( ( rec ( F , B ) |` _om ) ` y )
34 33 a1i 
 |-  ( ph -> A. y e. (/) ( ( rec ( F , B ) |` _om ) ` (/) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
35 nfv 
 |-  F/ y ( ph /\ z e. _om )
36 nfra1 
 |-  F/ y A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y )
37 35 36 nfan 
 |-  F/ y ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
38 16 ad3antlr 
 |-  ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) -> ( ( rec ( F , B ) |` _om ) ` suc z ) = ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) )
39 fveq2 
 |-  ( y = (/) -> ( ( rec ( F , B ) |` _om ) ` y ) = ( ( rec ( F , B ) |` _om ) ` (/) ) )
40 39 neeq2d 
 |-  ( y = (/) -> ( ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` (/) ) ) )
41 peano2b 
 |-  ( z e. _om <-> suc z e. _om )
42 elnn 
 |-  ( ( y e. suc z /\ suc z e. _om ) -> y e. _om )
43 42 ancoms 
 |-  ( ( suc z e. _om /\ y e. suc z ) -> y e. _om )
44 41 43 sylanb 
 |-  ( ( z e. _om /\ y e. suc z ) -> y e. _om )
45 44 ad4ant24 
 |-  ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) -> y e. _om )
46 nnsuc 
 |-  ( ( y e. _om /\ y =/= (/) ) -> E. x e. _om y = suc x )
47 45 46 sylan 
 |-  ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) -> E. x e. _om y = suc x )
48 fveq2 
 |-  ( y = x -> ( ( rec ( F , B ) |` _om ) ` y ) = ( ( rec ( F , B ) |` _om ) ` x ) )
49 48 neeq2d 
 |-  ( y = x -> ( ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) <-> ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` x ) ) )
50 simp-4r 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
51 simprr 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> y = suc x )
52 simpllr 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> y e. suc z )
53 51 52 eqeltrrd 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> suc x e. suc z )
54 nnord 
 |-  ( z e. _om -> Ord z )
55 54 ad5antlr 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> Ord z )
56 ordsucelsuc 
 |-  ( Ord z -> ( x e. z <-> suc x e. suc z ) )
57 55 56 syl 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( x e. z <-> suc x e. suc z ) )
58 53 57 mpbird 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> x e. z )
59 49 50 58 rspcdva 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` x ) )
60 simp-5l 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ph )
61 60 1 syl 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> F : A -1-1-> A )
62 26 ffvelcdmda 
 |-  ( ( ph /\ z e. _om ) -> ( ( rec ( F , B ) |` _om ) ` z ) e. A )
63 62 ad4antr 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( ( rec ( F , B ) |` _om ) ` z ) e. A )
64 simprl 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> x e. _om )
65 64 60 20 sylc 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( ( rec ( F , B ) |` _om ) ` x ) e. A )
66 f1fveq 
 |-  ( ( F : A -1-1-> A /\ ( ( ( rec ( F , B ) |` _om ) ` z ) e. A /\ ( ( rec ( F , B ) |` _om ) ` x ) e. A ) ) -> ( ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) = ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) <-> ( ( rec ( F , B ) |` _om ) ` z ) = ( ( rec ( F , B ) |` _om ) ` x ) ) )
67 66 necon3bid 
 |-  ( ( F : A -1-1-> A /\ ( ( ( rec ( F , B ) |` _om ) ` z ) e. A /\ ( ( rec ( F , B ) |` _om ) ` x ) e. A ) ) -> ( ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) <-> ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` x ) ) )
68 61 63 65 67 syl12anc 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) <-> ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` x ) ) )
69 59 68 mpbird 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) )
70 fveq2 
 |-  ( y = suc x -> ( ( rec ( F , B ) |` _om ) ` y ) = ( ( rec ( F , B ) |` _om ) ` suc x ) )
71 frsuc 
 |-  ( x e. _om -> ( ( rec ( F , B ) |` _om ) ` suc x ) = ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) )
72 70 71 sylan9eqr 
 |-  ( ( x e. _om /\ y = suc x ) -> ( ( rec ( F , B ) |` _om ) ` y ) = ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) )
73 72 adantl 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( ( rec ( F , B ) |` _om ) ` y ) = ( F ` ( ( rec ( F , B ) |` _om ) ` x ) ) )
74 69 73 neeqtrrd 
 |-  ( ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) /\ ( x e. _om /\ y = suc x ) ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
75 47 74 rexlimddv 
 |-  ( ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) /\ y =/= (/) ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
76 14 ffnd 
 |-  ( ph -> F Fn A )
77 76 adantr 
 |-  ( ( ph /\ z e. _om ) -> F Fn A )
78 77 62 fnfvelrnd 
 |-  ( ( ph /\ z e. _om ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) e. ran F )
79 11 adantr 
 |-  ( ( ph /\ z e. _om ) -> ( ( rec ( F , B ) |` _om ) ` (/) ) e. ( A \ ran F ) )
80 elneeldif 
 |-  ( ( ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) e. ran F /\ ( ( rec ( F , B ) |` _om ) ` (/) ) e. ( A \ ran F ) ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` (/) ) )
81 78 79 80 syl2anc 
 |-  ( ( ph /\ z e. _om ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` (/) ) )
82 81 ad2antrr 
 |-  ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` (/) ) )
83 40 75 82 pm2.61ne 
 |-  ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) -> ( F ` ( ( rec ( F , B ) |` _om ) ` z ) ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
84 38 83 eqnetrd 
 |-  ( ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) /\ y e. suc z ) -> ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
85 37 84 ralrimia 
 |-  ( ( ( ph /\ z e. _om ) /\ A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) -> A. y e. suc z ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) )
86 85 exp31 
 |-  ( ph -> ( z e. _om -> ( A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) -> A. y e. suc z ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) )
87 86 com12 
 |-  ( z e. _om -> ( ph -> ( A. y e. z ( ( rec ( F , B ) |` _om ) ` z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) -> A. y e. suc z ( ( rec ( F , B ) |` _om ) ` suc z ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) )
88 28 30 32 34 87 finds2 
 |-  ( x e. _om -> ( ph -> A. y e. x ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
89 rsp 
 |-  ( A. y e. x ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) -> ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
90 88 89 syl6com 
 |-  ( ph -> ( x e. _om -> ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) )
91 90 adantrd 
 |-  ( ph -> ( ( x e. _om /\ y e. _om ) -> ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) )
92 91 ralrimivv 
 |-  ( ph -> A. x e. _om A. y e. _om ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) )
93 omsson 
 |-  _om C_ On
94 onelfvnef1 
 |-  ( ( ( rec ( F , B ) |` _om ) : _om --> A /\ _om C_ On /\ A. x e. _om A. y e. _om ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) -> ( rec ( F , B ) |` _om ) : _om -1-1-> A )
95 93 94 mp3an2 
 |-  ( ( ( rec ( F , B ) |` _om ) : _om --> A /\ A. x e. _om A. y e. _om ( y e. x -> ( ( rec ( F , B ) |` _om ) ` x ) =/= ( ( rec ( F , B ) |` _om ) ` y ) ) ) -> ( rec ( F , B ) |` _om ) : _om -1-1-> A )
96 26 92 95 syl2anc 
 |-  ( ph -> ( rec ( F , B ) |` _om ) : _om -1-1-> A )