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 33520 |
. . . . . . . . . 10
⊢ <s Or
No |
4 | | sonr 5465 |
. . . . . . . . . 10
⊢ (( <s
Or No ∧ 𝐴 ∈ No )
→ ¬ 𝐴 <s 𝐴) |
5 | 3, 4 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ¬ 𝐴
<s 𝐴) |
6 | | breq2 5034 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵)) |
7 | 6 | notbid 321 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵)) |
8 | 5, 7 | syl5ibcom 248 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝐴 =
𝐵 → ¬ 𝐴 <s 𝐵)) |
9 | 8 | necon2ad 2949 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝐴 <s
𝐵 → 𝐴 ≠ 𝐵)) |
10 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → 𝐴 ≠ 𝐵)) |
11 | 10 | imp 410 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → 𝐴 ≠ 𝐵) |
12 | 11 | adantrl 716 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 ≠ 𝐵) |
13 | | nosepdm 33528 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵)) |
14 | 1, 2, 12, 13 | syl3anc 1372 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ (dom 𝐴 ∪ dom 𝐵)) |
15 | | unidm 4042 |
. . . . 5
⊢ (( bday ‘𝐴) ∪ ( bday
‘𝐴)) = ( bday ‘𝐴) |
16 | | simprl 771 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐴) = ( bday ‘𝐵)) |
17 | 16 | uneq2d 4053 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐴)) = (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
18 | 15, 17 | syl5reqr 2788 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐵)) = ( bday
‘𝐴)) |
19 | | bdayval 33492 |
. . . . . 6
⊢ (𝐴 ∈
No → ( bday ‘𝐴) = dom 𝐴) |
20 | 1, 19 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐴) = dom
𝐴) |
21 | | bdayval 33492 |
. . . . . 6
⊢ (𝐵 ∈
No → ( bday ‘𝐵) = dom 𝐵) |
22 | 2, 21 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐵) = dom
𝐵) |
23 | 20, 22 | uneq12d 4054 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (( bday
‘𝐴) ∪
( bday ‘𝐵)) = (dom 𝐴 ∪ dom 𝐵)) |
24 | 18, 23, 20 | 3eqtr3d 2781 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (dom 𝐴 ∪ dom 𝐵) = dom 𝐴) |
25 | 14, 24 | eleqtrd 2835 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴) |
26 | 25, 20 | eleqtrrd 2836 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴)) |