| Step | Hyp | Ref
| Expression |
| 1 | | df-fr 5637 |
. 2
⊢ (𝑅 Fr No
↔ ∀𝑎((𝑎 ⊆ No
∧ 𝑎 ≠ ∅)
→ ∃𝑝 ∈
𝑎 ∀𝑞 ∈ 𝑎 ¬ 𝑞𝑅𝑝)) |
| 2 | | bdayfun 27817 |
. . . . 5
⊢ Fun bday |
| 3 | | imassrn 6089 |
. . . . . . 7
⊢ ( bday “ 𝑎) ⊆ ran bday
|
| 4 | | bdayrn 27820 |
. . . . . . 7
⊢ ran bday = On |
| 5 | 3, 4 | sseqtri 4032 |
. . . . . 6
⊢ ( bday “ 𝑎) ⊆ On |
| 6 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ ( bday ‘𝑞) ∈ V |
| 7 | 6 | jctr 524 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈ 𝑎 → (𝑞 ∈ 𝑎 ∧ ( bday
‘𝑞) ∈
V)) |
| 8 | 7 | eximi 1835 |
. . . . . . . . . . 11
⊢
(∃𝑞 𝑞 ∈ 𝑎 → ∃𝑞(𝑞 ∈ 𝑎 ∧ ( bday
‘𝑞) ∈
V)) |
| 9 | | n0 4353 |
. . . . . . . . . . 11
⊢ (𝑎 ≠ ∅ ↔
∃𝑞 𝑞 ∈ 𝑎) |
| 10 | | df-rex 3071 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈
𝑎 (
bday ‘𝑞)
∈ V ↔ ∃𝑞(𝑞 ∈ 𝑎 ∧ ( bday
‘𝑞) ∈
V)) |
| 11 | 8, 9, 10 | 3imtr4i 292 |
. . . . . . . . . 10
⊢ (𝑎 ≠ ∅ →
∃𝑞 ∈ 𝑎 ( bday
‘𝑞) ∈
V) |
| 12 | | isset 3494 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑞) ∈ V ↔ ∃𝑝 𝑝 = ( bday
‘𝑞)) |
| 13 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ( bday
‘𝑞) ↔
( bday ‘𝑞) = 𝑝) |
| 14 | 13 | exbii 1848 |
. . . . . . . . . . . . 13
⊢
(∃𝑝 𝑝 = ( bday
‘𝑞) ↔
∃𝑝( bday ‘𝑞) = 𝑝) |
| 15 | 12, 14 | bitri 275 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑞) ∈ V ↔ ∃𝑝( bday
‘𝑞) = 𝑝) |
| 16 | 15 | rexbii 3094 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈
𝑎 (
bday ‘𝑞)
∈ V ↔ ∃𝑞
∈ 𝑎 ∃𝑝( bday
‘𝑞) = 𝑝) |
| 17 | | rexcom4 3288 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈
𝑎 ∃𝑝( bday
‘𝑞) = 𝑝 ↔ ∃𝑝∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝) |
| 18 | 16, 17 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈
𝑎 (
bday ‘𝑞)
∈ V ↔ ∃𝑝∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝) |
| 19 | 11, 18 | sylib 218 |
. . . . . . . . 9
⊢ (𝑎 ≠ ∅ →
∃𝑝∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝) |
| 20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∃𝑝∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝) |
| 21 | | bdayfn 27818 |
. . . . . . . . . . 11
⊢ bday Fn No
|
| 22 | | fvelimab 6981 |
. . . . . . . . . . 11
⊢ (( bday Fn No ∧ 𝑎 ⊆
No ) → (𝑝
∈ ( bday “ 𝑎) ↔ ∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝)) |
| 23 | 21, 22 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑎 ⊆
No → (𝑝 ∈
( bday “ 𝑎) ↔ ∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝)) |
| 24 | 23 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → (𝑝 ∈
( bday “ 𝑎) ↔ ∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝)) |
| 25 | 24 | exbidv 1921 |
. . . . . . . 8
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → (∃𝑝
𝑝 ∈ ( bday “ 𝑎) ↔ ∃𝑝∃𝑞 ∈ 𝑎 ( bday
‘𝑞) = 𝑝)) |
| 26 | 20, 25 | mpbird 257 |
. . . . . . 7
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∃𝑝
𝑝 ∈ ( bday “ 𝑎)) |
| 27 | | n0 4353 |
. . . . . . 7
⊢ (( bday “ 𝑎) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ ( bday
“ 𝑎)) |
| 28 | 26, 27 | sylibr 234 |
. . . . . 6
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ( bday “ 𝑎) ≠ ∅) |
| 29 | | onint 7810 |
. . . . . 6
⊢ ((( bday “ 𝑎) ⊆ On ∧ (
bday “ 𝑎)
≠ ∅) → ∩ ( bday
“ 𝑎) ∈
( bday “ 𝑎)) |
| 30 | 5, 28, 29 | sylancr 587 |
. . . . 5
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∩ ( bday
“ 𝑎) ∈
( bday “ 𝑎)) |
| 31 | | fvelima 6974 |
. . . . 5
⊢ ((Fun
bday ∧ ∩ ( bday “ 𝑎) ∈ ( bday
“ 𝑎)) →
∃𝑝 ∈ 𝑎 ( bday
‘𝑝) = ∩ ( bday “ 𝑎)) |
| 32 | 2, 30, 31 | sylancr 587 |
. . . 4
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∃𝑝
∈ 𝑎 ( bday ‘𝑝) = ∩ ( bday “ 𝑎)) |
| 33 | | fnfvima 7253 |
. . . . . . . . . 10
⊢ (( bday Fn No ∧ 𝑎 ⊆
No ∧ 𝑞 ∈
𝑎) → ( bday ‘𝑞) ∈ ( bday
“ 𝑎)) |
| 34 | 21, 33 | mp3an1 1450 |
. . . . . . . . 9
⊢ ((𝑎 ⊆
No ∧ 𝑞 ∈
𝑎) → ( bday ‘𝑞) ∈ ( bday
“ 𝑎)) |
| 35 | 34 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ 𝑞 ∈
𝑎) → ( bday ‘𝑞) ∈ ( bday
“ 𝑎)) |
| 36 | | onnmin 7818 |
. . . . . . . 8
⊢ ((( bday “ 𝑎) ⊆ On ∧ (
bday ‘𝑞)
∈ ( bday “ 𝑎)) → ¬ ( bday
‘𝑞) ∈
∩ ( bday “ 𝑎)) |
| 37 | 5, 35, 36 | sylancr 587 |
. . . . . . 7
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ 𝑞 ∈
𝑎) → ¬ ( bday ‘𝑞) ∈ ∩ ( bday “ 𝑎)) |
| 38 | 37 | ralrimiva 3146 |
. . . . . 6
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∀𝑞
∈ 𝑎 ¬ ( bday ‘𝑞) ∈ ∩ ( bday “ 𝑎)) |
| 39 | | eleq2 2830 |
. . . . . . . 8
⊢ (( bday ‘𝑝) = ∩ ( bday “ 𝑎) → (( bday
‘𝑞) ∈
( bday ‘𝑝) ↔ ( bday
‘𝑞) ∈
∩ ( bday “ 𝑎))) |
| 40 | 39 | notbid 318 |
. . . . . . 7
⊢ (( bday ‘𝑝) = ∩ ( bday “ 𝑎) → (¬ ( bday
‘𝑞) ∈
( bday ‘𝑝) ↔ ¬ ( bday
‘𝑞) ∈
∩ ( bday “ 𝑎))) |
| 41 | 40 | ralbidv 3178 |
. . . . . 6
⊢ (( bday ‘𝑝) = ∩ ( bday “ 𝑎) → (∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝) ↔ ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
∩ ( bday “ 𝑎))) |
| 42 | 38, 41 | syl5ibrcom 247 |
. . . . 5
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → (( bday ‘𝑝) = ∩ ( bday “ 𝑎) → ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 43 | 42 | reximdv 3170 |
. . . 4
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → (∃𝑝
∈ 𝑎 ( bday ‘𝑝) = ∩ ( bday “ 𝑎) → ∃𝑝 ∈ 𝑎 ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 44 | 32, 43 | mpd 15 |
. . 3
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∃𝑝
∈ 𝑎 ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝)) |
| 45 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → 𝑎 ⊆ No
) |
| 46 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → 𝑞 ∈ 𝑎) |
| 47 | 45, 46 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → 𝑞 ∈ No
) |
| 48 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → 𝑝 ∈ 𝑎) |
| 49 | 45, 48 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → 𝑝 ∈ No
) |
| 50 | | lrrec.1 |
. . . . . . . . 9
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} |
| 51 | 50 | lrrecval2 27973 |
. . . . . . . 8
⊢ ((𝑞 ∈
No ∧ 𝑝 ∈
No ) → (𝑞𝑅𝑝 ↔ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 52 | 47, 49, 51 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → (𝑞𝑅𝑝 ↔ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 53 | 52 | notbid 318 |
. . . . . 6
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ (𝑝 ∈
𝑎 ∧ 𝑞 ∈ 𝑎)) → (¬ 𝑞𝑅𝑝 ↔ ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 54 | 53 | anassrs 467 |
. . . . 5
⊢ ((((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ 𝑝 ∈
𝑎) ∧ 𝑞 ∈ 𝑎) → (¬ 𝑞𝑅𝑝 ↔ ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 55 | 54 | ralbidva 3176 |
. . . 4
⊢ (((𝑎 ⊆
No ∧ 𝑎 ≠
∅) ∧ 𝑝 ∈
𝑎) → (∀𝑞 ∈ 𝑎 ¬ 𝑞𝑅𝑝 ↔ ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 56 | 55 | rexbidva 3177 |
. . 3
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → (∃𝑝
∈ 𝑎 ∀𝑞 ∈ 𝑎 ¬ 𝑞𝑅𝑝 ↔ ∃𝑝 ∈ 𝑎 ∀𝑞 ∈ 𝑎 ¬ ( bday
‘𝑞) ∈
( bday ‘𝑝))) |
| 57 | 44, 56 | mpbird 257 |
. 2
⊢ ((𝑎 ⊆
No ∧ 𝑎 ≠
∅) → ∃𝑝
∈ 𝑎 ∀𝑞 ∈ 𝑎 ¬ 𝑞𝑅𝑝) |
| 58 | 1, 57 | mpgbir 1799 |
1
⊢ 𝑅 Fr No
|