Proof of Theorem nodenselem4
Step | Hyp | Ref
| Expression |
1 | | ssrab2 3650 |
. 2
⊢ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On |
2 | | sltirr 31069 |
. . . . . . 7
⊢ (𝐴 ∈
No → ¬ 𝐴
<s 𝐴) |
3 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵)) |
4 | 3 | biimprcd 239 |
. . . . . . . 8
⊢ (𝐴 <s 𝐵 → (𝐴 = 𝐵 → 𝐴 <s 𝐴)) |
5 | 4 | con3d 147 |
. . . . . . 7
⊢ (𝐴 <s 𝐵 → (¬ 𝐴 <s 𝐴 → ¬ 𝐴 = 𝐵)) |
6 | 2, 5 | syl5com 31 |
. . . . . 6
⊢ (𝐴 ∈
No → (𝐴 <s
𝐵 → ¬ 𝐴 = 𝐵)) |
7 | 6 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → ¬ 𝐴 = 𝐵)) |
8 | | nofnbday 31049 |
. . . . . . . 8
⊢ (𝐴 ∈
No → 𝐴 Fn
( bday ‘𝐴)) |
9 | | nofnbday 31049 |
. . . . . . . 8
⊢ (𝐵 ∈
No → 𝐵 Fn
( bday ‘𝐵)) |
10 | | eqfnfv2 6220 |
. . . . . . . 8
⊢ ((𝐴 Fn ( bday
‘𝐴) ∧
𝐵 Fn ( bday ‘𝐵)) → (𝐴 = 𝐵 ↔ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)))) |
11 | 8, 9, 10 | syl2an 493 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 = 𝐵 ↔ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)))) |
12 | 11 | notbid 307 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ 𝐴 = 𝐵 ↔ ¬ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)))) |
13 | | ianor 508 |
. . . . . . 7
⊢ (¬
(( bday ‘𝐴) = ( bday
‘𝐵) ∧
∀𝑎 ∈ ( bday ‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)) ↔ (¬ ( bday
‘𝐴) = ( bday ‘𝐵) ∨ ¬ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎))) |
14 | | bdayelon 31079 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐴) ∈ On |
15 | 14 | onordi 5749 |
. . . . . . . . . . 11
⊢ Ord
( bday ‘𝐴) |
16 | | bdayelon 31079 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐵) ∈ On |
17 | 16 | onordi 5749 |
. . . . . . . . . . 11
⊢ Ord
( bday ‘𝐵) |
18 | | ordtri3 5676 |
. . . . . . . . . . 11
⊢ ((Ord
( bday ‘𝐴) ∧ Ord ( bday
‘𝐵)) →
(( bday ‘𝐴) = ( bday
‘𝐵) ↔
¬ (( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴)))) |
19 | 15, 17, 18 | mp2an 704 |
. . . . . . . . . 10
⊢ (( bday ‘𝐴) = ( bday
‘𝐵) ↔
¬ (( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴))) |
20 | 19 | con2bii 346 |
. . . . . . . . 9
⊢ ((( bday ‘𝐴) ∈ ( bday
‘𝐵) ∨
( bday ‘𝐵) ∈ ( bday
‘𝐴)) ↔
¬ ( bday ‘𝐴) = ( bday
‘𝐵)) |
21 | | nodenselem3 31082 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) ∈
( bday ‘𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
22 | | nodenselem3 31082 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (( bday
‘𝐵) ∈
( bday ‘𝐴) → ∃𝑎 ∈ On (𝐵‘𝑎) ≠ (𝐴‘𝑎))) |
23 | | necom 2835 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝑎) ≠ (𝐴‘𝑎) ↔ (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
24 | 23 | rexbii 3023 |
. . . . . . . . . . . 12
⊢
(∃𝑎 ∈ On
(𝐵‘𝑎) ≠ (𝐴‘𝑎) ↔ ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
25 | 22, 24 | syl6ib 240 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
No ∧ 𝐴 ∈
No ) → (( bday
‘𝐵) ∈
( bday ‘𝐴) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
26 | 25 | ancoms 468 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐵) ∈
( bday ‘𝐴) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
27 | 21, 26 | jaod 394 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( bday
‘𝐴) ∈
( bday ‘𝐵) ∨ ( bday
‘𝐵) ∈
( bday ‘𝐴)) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
28 | 20, 27 | syl5bir 232 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ ( bday
‘𝐴) = ( bday ‘𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
29 | | rexnal 2978 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
( bday ‘𝐴) ¬ (𝐴‘𝑎) = (𝐵‘𝑎) ↔ ¬ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)) |
30 | 14 | onssi 6929 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐴) ⊆ On |
31 | | ssrexv 3630 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝐴) ⊆ On → (∃𝑎 ∈ (
bday ‘𝐴) ¬
(𝐴‘𝑎) = (𝐵‘𝑎) → ∃𝑎 ∈ On ¬ (𝐴‘𝑎) = (𝐵‘𝑎))) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈
( bday ‘𝐴) ¬ (𝐴‘𝑎) = (𝐵‘𝑎) → ∃𝑎 ∈ On ¬ (𝐴‘𝑎) = (𝐵‘𝑎)) |
33 | | df-ne 2782 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ ¬ (𝐴‘𝑎) = (𝐵‘𝑎)) |
34 | 33 | rexbii 3023 |
. . . . . . . . . . 11
⊢
(∃𝑎 ∈ On
(𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ ∃𝑎 ∈ On ¬ (𝐴‘𝑎) = (𝐵‘𝑎)) |
35 | 32, 34 | sylibr 223 |
. . . . . . . . . 10
⊢
(∃𝑎 ∈
( bday ‘𝐴) ¬ (𝐴‘𝑎) = (𝐵‘𝑎) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
36 | 29, 35 | sylbir 224 |
. . . . . . . . 9
⊢ (¬
∀𝑎 ∈ ( bday ‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
37 | 36 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
38 | 28, 37 | jaod 394 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((¬ ( bday
‘𝐴) = ( bday ‘𝐵) ∨ ¬ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
39 | 13, 38 | syl5bi 231 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ ∀𝑎 ∈ ( bday
‘𝐴)(𝐴‘𝑎) = (𝐵‘𝑎)) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
40 | 12, 39 | sylbid 229 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ 𝐴 = 𝐵 → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
41 | 7, 40 | syld 46 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎))) |
42 | 41 | imp 444 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
43 | | rabn0 3912 |
. . 3
⊢ ({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅ ↔ ∃𝑎 ∈ On (𝐴‘𝑎) ≠ (𝐵‘𝑎)) |
44 | 42, 43 | sylibr 223 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) |
45 | | oninton 6892 |
. 2
⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
46 | 1, 44, 45 | sylancr 694 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |