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