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 |