Proof of Theorem nodenselem5
| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 ∈ No
) |
| 2 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐵 ∈ No
) |
| 3 | | sltso 27721 |
. . . . . . . . . 10
⊢ <s Or
No |
| 4 | | sonr 5616 |
. . . . . . . . . 10
⊢ (( <s
Or No ∧ 𝐴 ∈ No )
→ ¬ 𝐴 <s 𝐴) |
| 5 | 3, 4 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ¬ 𝐴
<s 𝐴) |
| 6 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵)) |
| 7 | 6 | notbid 318 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵)) |
| 8 | 5, 7 | syl5ibcom 245 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝐴 =
𝐵 → ¬ 𝐴 <s 𝐵)) |
| 9 | 8 | necon2ad 2955 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝐴 <s
𝐵 → 𝐴 ≠ 𝐵)) |
| 10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → 𝐴 ≠ 𝐵)) |
| 11 | 10 | imp 406 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → 𝐴 ≠ 𝐵) |
| 12 | 11 | adantrl 716 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 ≠ 𝐵) |
| 13 | | nosepdm 27729 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵)) |
| 14 | 1, 2, 12, 13 | syl3anc 1373 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵)) |
| 15 | | simprl 771 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐴) = ( bday ‘𝐵)) |
| 16 | 15 | uneq2d 4168 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐴)) = (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
| 17 | | unidm 4157 |
. . . . 5
⊢ (( bday ‘𝐴) ∪ ( bday
‘𝐴)) = ( bday ‘𝐴) |
| 18 | 16, 17 | eqtr3di 2792 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐵)) = ( bday
‘𝐴)) |
| 19 | | bdayval 27693 |
. . . . . 6
⊢ (𝐴 ∈
No → ( bday ‘𝐴) = dom 𝐴) |
| 20 | 1, 19 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐴) = dom
𝐴) |
| 21 | | bdayval 27693 |
. . . . . 6
⊢ (𝐵 ∈
No → ( bday ‘𝐵) = dom 𝐵) |
| 22 | 2, 21 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐵) = dom
𝐵) |
| 23 | 20, 22 | uneq12d 4169 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐵)) = (dom 𝐴 ∪ dom 𝐵)) |
| 24 | 18, 23, 20 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (dom 𝐴 ∪ dom 𝐵) = dom 𝐴) |
| 25 | 14, 24 | eleqtrd 2843 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴) |
| 26 | 25, 20 | eleqtrrd 2844 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴)) |