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 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) }
Assertion lrrecfr 𝑅 Fr No

Proof

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