| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | imassrn 6089 | . . . . . 6
⊢ ( bday  “ 𝐴) ⊆ ran  bday | 
| 2 |  | bdayrn 27820 | . . . . . 6
⊢ ran  bday  = On | 
| 3 | 1, 2 | sseqtri 4032 | . . . . 5
⊢ ( bday  “ 𝐴) ⊆ On | 
| 4 |  | bdaydm 27819 | . . . . . . . . . . 11
⊢ dom  bday  =  No | 
| 5 | 4 | sseq2i 4013 | . . . . . . . . . 10
⊢ (𝐴 ⊆ dom  bday  ↔ 𝐴 ⊆  No
) | 
| 6 |  | bdayfun 27817 | . . . . . . . . . . 11
⊢ Fun  bday | 
| 7 |  | funfvima2 7251 | . . . . . . . . . . 11
⊢ ((Fun
 bday  ∧ 𝐴 ⊆ dom  bday
) → (𝑥 ∈
𝐴 → ( bday ‘𝑥) ∈ ( bday 
“ 𝐴))) | 
| 8 | 6, 7 | mpan 690 | . . . . . . . . . 10
⊢ (𝐴 ⊆ dom  bday  → (𝑥 ∈ 𝐴 → ( bday
‘𝑥) ∈
( bday  “ 𝐴))) | 
| 9 | 5, 8 | sylbir 235 | . . . . . . . . 9
⊢ (𝐴 ⊆ 
No  → (𝑥 ∈
𝐴 → ( bday ‘𝑥) ∈ ( bday 
“ 𝐴))) | 
| 10 |  | elex2 2818 | . . . . . . . . 9
⊢ (( bday ‘𝑥) ∈ ( bday 
“ 𝐴) →
∃𝑤 𝑤 ∈ ( bday 
“ 𝐴)) | 
| 11 | 9, 10 | syl6 35 | . . . . . . . 8
⊢ (𝐴 ⊆ 
No  → (𝑥 ∈
𝐴 → ∃𝑤 𝑤 ∈ ( bday 
“ 𝐴))) | 
| 12 | 11 | exlimdv 1933 | . . . . . . 7
⊢ (𝐴 ⊆ 
No  → (∃𝑥
𝑥 ∈ 𝐴 → ∃𝑤 𝑤 ∈ ( bday 
“ 𝐴))) | 
| 13 |  | n0 4353 | . . . . . . 7
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) | 
| 14 |  | n0 4353 | . . . . . . 7
⊢ (( bday  “ 𝐴) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ( bday 
“ 𝐴)) | 
| 15 | 12, 13, 14 | 3imtr4g 296 | . . . . . 6
⊢ (𝐴 ⊆ 
No  → (𝐴 ≠
∅ → ( bday  “ 𝐴) ≠ ∅)) | 
| 16 | 15 | impcom 407 | . . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No ) → ( bday  “ 𝐴) ≠ ∅) | 
| 17 |  | onint 7810 | . . . . 5
⊢ ((( bday  “ 𝐴) ⊆ On ∧ (
bday  “ 𝐴)
≠ ∅) → ∩ ( bday
 “ 𝐴) ∈
( bday  “ 𝐴)) | 
| 18 | 3, 16, 17 | sylancr 587 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No ) → ∩ ( bday
 “ 𝐴) ∈
( bday  “ 𝐴)) | 
| 19 |  | bdayfn 27818 | . . . . . 6
⊢  bday  Fn  No | 
| 20 |  | fvelimab 6981 | . . . . . 6
⊢ (( bday  Fn  No  ∧ 𝐴 ⊆ 
No ) → (∩ ( bday
 “ 𝐴) ∈
( bday  “ 𝐴) ↔ ∃𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴))) | 
| 21 | 19, 20 | mpan 690 | . . . . 5
⊢ (𝐴 ⊆ 
No  → (∩ ( bday
 “ 𝐴) ∈
( bday  “ 𝐴) ↔ ∃𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴))) | 
| 22 | 21 | adantl 481 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No ) → (∩ ( bday
 “ 𝐴) ∈
( bday  “ 𝐴) ↔ ∃𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴))) | 
| 23 | 18, 22 | mpbid 232 | . . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No ) → ∃𝑤
∈ 𝐴 ( bday ‘𝑤) = ∩ ( bday  “ 𝐴)) | 
| 24 | 23 | 3adant3 1133 | . 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴)) | 
| 25 |  | ssel 3977 | . . . . . . . . 9
⊢ (𝐴 ⊆ 
No  → (𝑤 ∈
𝐴 → 𝑤 ∈  No
)) | 
| 26 |  | ssel 3977 | . . . . . . . . 9
⊢ (𝐴 ⊆ 
No  → (𝑡 ∈
𝐴 → 𝑡 ∈  No
)) | 
| 27 | 25, 26 | anim12d 609 | . . . . . . . 8
⊢ (𝐴 ⊆ 
No  → ((𝑤
∈ 𝐴 ∧ 𝑡 ∈ 𝐴) → (𝑤 ∈  No 
∧ 𝑡 ∈  No ))) | 
| 28 | 27 | imp 406 | . . . . . . 7
⊢ ((𝐴 ⊆ 
No  ∧ (𝑤 ∈
𝐴 ∧ 𝑡 ∈ 𝐴)) → (𝑤 ∈  No 
∧ 𝑡 ∈  No )) | 
| 29 | 28 | ad2ant2r 747 | . . . . . 6
⊢ (((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)))) → (𝑤 ∈  No 
∧ 𝑡 ∈  No )) | 
| 30 |  | nocvxminlem 27822 | . . . . . . 7
⊢ ((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴))) → ¬ 𝑤 <s 𝑡)) | 
| 31 | 30 | imp 406 | . . . . . 6
⊢ (((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)))) → ¬ 𝑤 <s 𝑡) | 
| 32 |  | ancom 460 | . . . . . . . . 9
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ↔ (𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) | 
| 33 |  | ancom 460 | . . . . . . . . 9
⊢ ((( bday ‘𝑤) = ∩ ( bday  “ 𝐴) ∧ ( bday
‘𝑡) = ∩ ( bday  “ 𝐴)) ↔ (( bday ‘𝑡) = ∩ ( bday  “ 𝐴) ∧ ( bday
‘𝑤) = ∩ ( bday  “ 𝐴))) | 
| 34 | 32, 33 | anbi12i 628 | . . . . . . . 8
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴))) ↔ ((𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (( bday
‘𝑡) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑤) =
∩ ( bday  “ 𝐴)))) | 
| 35 |  | nocvxminlem 27822 | . . . . . . . 8
⊢ ((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑡 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (( bday
‘𝑡) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑤) =
∩ ( bday  “ 𝐴))) → ¬ 𝑡 <s 𝑤)) | 
| 36 | 34, 35 | biimtrid 242 | . . . . . . 7
⊢ ((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴))) → ¬ 𝑡 <s 𝑤)) | 
| 37 | 36 | imp 406 | . . . . . 6
⊢ (((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)))) → ¬ 𝑡 <s 𝑤) | 
| 38 |  | slttrieq2 27795 | . . . . . . 7
⊢ ((𝑤 ∈ 
No  ∧ 𝑡 ∈
 No ) → (𝑤 = 𝑡 ↔ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤))) | 
| 39 | 38 | biimpar 477 | . . . . . 6
⊢ (((𝑤 ∈ 
No  ∧ 𝑡 ∈
 No ) ∧ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤)) → 𝑤 = 𝑡) | 
| 40 | 29, 31, 37, 39 | syl12anc 837 | . . . . 5
⊢ (((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) ∧ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) ∧ (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)))) → 𝑤 = 𝑡) | 
| 41 | 40 | exp32 420 | . . . 4
⊢ ((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴) → ((( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)) → 𝑤 = 𝑡))) | 
| 42 | 41 | ralrimivv 3200 | . . 3
⊢ ((𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐴 ((( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)) → 𝑤 = 𝑡)) | 
| 43 | 42 | 3adant1 1131 | . 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐴 ((( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)) → 𝑤 = 𝑡)) | 
| 44 |  | fveqeq2 6915 | . . 3
⊢ (𝑤 = 𝑡 → (( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ↔ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴))) | 
| 45 | 44 | reu4 3737 | . 2
⊢
(∃!𝑤 ∈
𝐴 (
bday ‘𝑤) =
∩ ( bday  “ 𝐴) ↔ (∃𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐴 ((( bday
‘𝑤) = ∩ ( bday  “ 𝐴) ∧ (
bday ‘𝑡) =
∩ ( bday  “ 𝐴)) → 𝑤 = 𝑡))) | 
| 46 | 24, 43, 45 | sylanbrc 583 | 1
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ 
No  ∧ ∀𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈  No 
((𝑥 <s 𝑧 ∧ 𝑧 <s 𝑦) → 𝑧 ∈ 𝐴)) → ∃!𝑤 ∈ 𝐴 ( bday
‘𝑤) = ∩ ( bday  “ 𝐴)) |