Metamath Proof Explorer

Theorem lrrecfr

Description: Now we show that R is founded over No . (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypothesis lrrec.1 
|- R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
Assertion lrrecfr 
|- R Fr No

Proof

Step Hyp Ref Expression
1 lrrec.1 
 |-  R = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
2 df-fr 
 |-  ( R Fr No <-> A. a ( ( a C_ No /\ a =/= (/) ) -> E. p e. a A. q e. a -. q R p ) )
3 bdayfun 
 |-  Fun bday
4 imassrn 
 |-  ( bday " a ) C_ ran bday
5 bdayrn 
 |-  ran bday = On
6 4 5 sseqtri 
 |-  ( bday " a ) C_ On
7 fvex 
 |-  ( bday ` q ) e. _V
8 7 jctr 
 |-  ( q e. a -> ( q e. a /\ ( bday ` q ) e. _V ) )
9 8 eximi 
 |-  ( E. q q e. a -> E. q ( q e. a /\ ( bday ` q ) e. _V ) )
10 n0 
 |-  ( a =/= (/) <-> E. q q e. a )
11 df-rex 
 |-  ( E. q e. a ( bday ` q ) e. _V <-> E. q ( q e. a /\ ( bday ` q ) e. _V ) )
12 9 10 11 3imtr4i 
 |-  ( a =/= (/) -> E. q e. a ( bday ` q ) e. _V )
13 isset 
 |-  ( ( bday ` q ) e. _V <-> E. p p = ( bday ` q ) )
14 eqcom 
 |-  ( p = ( bday ` q ) <-> ( bday ` q ) = p )
15 14 exbii 
 |-  ( E. p p = ( bday ` q ) <-> E. p ( bday ` q ) = p )
16 13 15 bitri 
 |-  ( ( bday ` q ) e. _V <-> E. p ( bday ` q ) = p )
17 16 rexbii 
 |-  ( E. q e. a ( bday ` q ) e. _V <-> E. q e. a E. p ( bday ` q ) = p )
18 rexcom4 
 |-  ( E. q e. a E. p ( bday ` q ) = p <-> E. p E. q e. a ( bday ` q ) = p )
19 17 18 bitri 
 |-  ( E. q e. a ( bday ` q ) e. _V <-> E. p E. q e. a ( bday ` q ) = p )
20 12 19 sylib 
 |-  ( a =/= (/) -> E. p E. q e. a ( bday ` q ) = p )
21 20 adantl 
 |-  ( ( a C_ No /\ a =/= (/) ) -> E. p E. q e. a ( bday ` q ) = p )
22 bdayfn 
 |-  bday Fn No
23 fvelimab 
 |-  ( ( bday Fn No /\ a C_ No ) -> ( p e. ( bday " a ) <-> E. q e. a ( bday ` q ) = p ) )
24 22 23 mpan 
 |-  ( a C_ No -> ( p e. ( bday " a ) <-> E. q e. a ( bday ` q ) = p ) )
25 24 adantr 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( p e. ( bday " a ) <-> E. q e. a ( bday ` q ) = p ) )
26 25 exbidv 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( E. p p e. ( bday " a ) <-> E. p E. q e. a ( bday ` q ) = p ) )
27 21 26 mpbird 
 |-  ( ( a C_ No /\ a =/= (/) ) -> E. p p e. ( bday " a ) )
28 n0 
 |-  ( ( bday " a ) =/= (/) <-> E. p p e. ( bday " a ) )
29 27 28 sylibr 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( bday " a ) =/= (/) )
30 onint 
 |-  ( ( ( bday " a ) C_ On /\ ( bday " a ) =/= (/) ) -> |^| ( bday " a ) e. ( bday " a ) )
31 6 29 30 sylancr 
 |-  ( ( a C_ No /\ a =/= (/) ) -> |^| ( bday " a ) e. ( bday " a ) )
32 fvelima 
 |-  ( ( Fun bday /\ |^| ( bday " a ) e. ( bday " a ) ) -> E. p e. a ( bday ` p ) = |^| ( bday " a ) )
33 3 31 32 sylancr 
 |-  ( ( a C_ No /\ a =/= (/) ) -> E. p e. a ( bday ` p ) = |^| ( bday " a ) )
34 fnfvima 
 |-  ( ( bday Fn No /\ a C_ No /\ q e. a ) -> ( bday ` q ) e. ( bday " a ) )
35 22 34 mp3an1 
 |-  ( ( a C_ No /\ q e. a ) -> ( bday ` q ) e. ( bday " a ) )
36 35 adantlr 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ q e. a ) -> ( bday ` q ) e. ( bday " a ) )
37 onnmin 
 |-  ( ( ( bday " a ) C_ On /\ ( bday ` q ) e. ( bday " a ) ) -> -. ( bday ` q ) e. |^| ( bday " a ) )
38 6 36 37 sylancr 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ q e. a ) -> -. ( bday ` q ) e. |^| ( bday " a ) )
39 38 ralrimiva 
 |-  ( ( a C_ No /\ a =/= (/) ) -> A. q e. a -. ( bday ` q ) e. |^| ( bday " a ) )
40 eleq2 
 |-  ( ( bday ` p ) = |^| ( bday " a ) -> ( ( bday ` q ) e. ( bday ` p ) <-> ( bday ` q ) e. |^| ( bday " a ) ) )
41 40 notbid 
 |-  ( ( bday ` p ) = |^| ( bday " a ) -> ( -. ( bday ` q ) e. ( bday ` p ) <-> -. ( bday ` q ) e. |^| ( bday " a ) ) )
42 41 ralbidv 
 |-  ( ( bday ` p ) = |^| ( bday " a ) -> ( A. q e. a -. ( bday ` q ) e. ( bday ` p ) <-> A. q e. a -. ( bday ` q ) e. |^| ( bday " a ) ) )
43 39 42 syl5ibrcom 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( ( bday ` p ) = |^| ( bday " a ) -> A. q e. a -. ( bday ` q ) e. ( bday ` p ) ) )
44 43 reximdv 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( E. p e. a ( bday ` p ) = |^| ( bday " a ) -> E. p e. a A. q e. a -. ( bday ` q ) e. ( bday ` p ) ) )
45 33 44 mpd 
 |-  ( ( a C_ No /\ a =/= (/) ) -> E. p e. a A. q e. a -. ( bday ` q ) e. ( bday ` p ) )
46 simpll 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> a C_ No )
47 simprr 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> q e. a )
48 46 47 sseldd 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> q e. No )
49 simprl 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> p e. a )
50 46 49 sseldd 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> p e. No )
51 1 lrrecval2 
 |-  ( ( q e. No /\ p e. No ) -> ( q R p <-> ( bday ` q ) e. ( bday ` p ) ) )
52 48 50 51 syl2anc 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> ( q R p <-> ( bday ` q ) e. ( bday ` p ) ) )
53 52 notbid 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ ( p e. a /\ q e. a ) ) -> ( -. q R p <-> -. ( bday ` q ) e. ( bday ` p ) ) )
54 53 anassrs 
 |-  ( ( ( ( a C_ No /\ a =/= (/) ) /\ p e. a ) /\ q e. a ) -> ( -. q R p <-> -. ( bday ` q ) e. ( bday ` p ) ) )
55 54 ralbidva 
 |-  ( ( ( a C_ No /\ a =/= (/) ) /\ p e. a ) -> ( A. q e. a -. q R p <-> A. q e. a -. ( bday ` q ) e. ( bday ` p ) ) )
56 55 rexbidva 
 |-  ( ( a C_ No /\ a =/= (/) ) -> ( E. p e. a A. q e. a -. q R p <-> E. p e. a A. q e. a -. ( bday ` q ) e. ( bday ` p ) ) )
57 45 56 mpbird 
 |-  ( ( a C_ No /\ a =/= (/) ) -> E. p e. a A. q e. a -. q R p )
58 2 57 mpgbir 
 |-  R Fr No