Proof of Theorem nodenselem3
Step | Hyp | Ref
| Expression |
1 | | bdayval 31045 |
. . . 4
⊢ (𝐵 ∈
No → ( bday ‘𝐵) = dom 𝐵) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( bday
‘𝐵) = dom
𝐵) |
3 | 2 | eleq2d 2673 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) ∈
( bday ‘𝐵) ↔ ( bday
‘𝐴) ∈ dom
𝐵)) |
4 | | bdayelon 31079 |
. . . 4
⊢ ( bday ‘𝐴) ∈ On |
5 | | nosgnn0 31055 |
. . . . . . . . 9
⊢ ¬
∅ ∈ {1𝑜, 2𝑜} |
6 | | norn 31048 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
No → ran 𝐵
⊆ {1𝑜, 2𝑜}) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → ran 𝐵 ⊆ {1𝑜,
2𝑜}) |
8 | | nofun 31046 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
No → Fun 𝐵) |
9 | | fvelrn 6260 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐵 ∧ ( bday ‘𝐴) ∈ dom 𝐵) → (𝐵‘( bday
‘𝐴)) ∈
ran 𝐵) |
10 | 8, 9 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → (𝐵‘( bday
‘𝐴)) ∈
ran 𝐵) |
11 | 7, 10 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → (𝐵‘( bday
‘𝐴)) ∈
{1𝑜, 2𝑜}) |
12 | | eleq1 2676 |
. . . . . . . . . 10
⊢ ((𝐵‘(
bday ‘𝐴)) =
∅ → ((𝐵‘( bday
‘𝐴)) ∈
{1𝑜, 2𝑜} ↔ ∅ ∈
{1𝑜, 2𝑜})) |
13 | 11, 12 | syl5ibcom 234 |
. . . . . . . . 9
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → ((𝐵‘( bday
‘𝐴)) = ∅
→ ∅ ∈ {1𝑜,
2𝑜})) |
14 | 5, 13 | mtoi 189 |
. . . . . . . 8
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → ¬ (𝐵‘( bday
‘𝐴)) =
∅) |
15 | 14 | neqned 2789 |
. . . . . . 7
⊢ ((𝐵 ∈
No ∧ ( bday ‘𝐴) ∈ dom 𝐵) → (𝐵‘( bday
‘𝐴)) ≠
∅) |
16 | 15 | adantll 746 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ( bday
‘𝐴) ∈ dom
𝐵) → (𝐵‘(
bday ‘𝐴)) ≠
∅) |
17 | | fvnobday 31081 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝐴‘( bday
‘𝐴)) =
∅) |
18 | 17 | ad2antrr 758 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ( bday
‘𝐴) ∈ dom
𝐵) → (𝐴‘(
bday ‘𝐴)) =
∅) |
19 | 16, 18 | neeqtrrd 2856 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ( bday
‘𝐴) ∈ dom
𝐵) → (𝐵‘(
bday ‘𝐴)) ≠
(𝐴‘( bday ‘𝐴))) |
20 | 19 | necomd 2837 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ( bday
‘𝐴) ∈ dom
𝐵) → (𝐴‘(
bday ‘𝐴)) ≠
(𝐵‘( bday ‘𝐴))) |
21 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = ( bday
‘𝐴) →
(𝐴‘𝑎) = (𝐴‘( bday
‘𝐴))) |
22 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = ( bday
‘𝐴) →
(𝐵‘𝑎) = (𝐵‘( bday
‘𝐴))) |
23 | 21, 22 | neeq12d 2843 |
. . . . 5
⊢ (𝑎 = ( bday
‘𝐴) →
((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘( bday
‘𝐴)) ≠
(𝐵‘( bday ‘𝐴)))) |
24 | 23 | rspcev 3282 |
. . . 4
⊢ ((( bday ‘𝐴) ∈ On ∧ (𝐴‘( bday
‘𝐴)) ≠
(𝐵‘( bday ‘𝐴))) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
25 | 4, 20, 24 | sylancr 694 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ( bday
‘𝐴) ∈ dom
𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
26 | 25 | ex 449 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) ∈ dom
𝐵 → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
27 | 3, 26 | sylbid 229 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) ∈
( bday ‘𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |