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 L y R y
Assertion lrrecfr R Fr No

Proof

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