Proof of Theorem nodenselem7
Step | Hyp | Ref
| Expression |
1 | | nodenselem4 31083 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
2 | 1 | adantrl 748 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
3 | | onelon 5665 |
. . . . 5
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝐶 ∈ On) |
4 | 3 | ex 449 |
. . . 4
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → 𝐶 ∈ On)) |
5 | 2, 4 | syl 17 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → 𝐶 ∈ On)) |
6 | 2, 3 | sylan 487 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝐶 ∈ On) |
7 | | ontri1 5674 |
. . . . . . . . . . . . . 14
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝐶 ∈ On) → (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶 ↔ ¬ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
8 | 7 | con2bid 343 |
. . . . . . . . . . . . 13
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝐶 ∈ On) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶)) |
9 | 8 | biimpd 218 |
. . . . . . . . . . . 12
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝐶 ∈ On) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶)) |
10 | 9 | ex 449 |
. . . . . . . . . . 11
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → (𝐶 ∈ On → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶))) |
11 | 10 | com23 84 |
. . . . . . . . . 10
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐶 ∈ On → ¬ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶))) |
12 | 2, 11 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐶 ∈ On → ¬ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶))) |
13 | 12 | imp 444 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐶 ∈ On → ¬ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶)) |
14 | 6, 13 | mpd 15 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶) |
15 | | intss1 4427 |
. . . . . . 7
⊢ (𝐶 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝐶) |
16 | 14, 15 | nsyl 134 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ 𝐶 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
17 | 16 | ex 449 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ 𝐶 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
18 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑎 = 𝐶 → (𝐴‘𝑎) = (𝐴‘𝐶)) |
19 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑎 = 𝐶 → (𝐵‘𝑎) = (𝐵‘𝐶)) |
20 | 18, 19 | neeq12d 2843 |
. . . . . . 7
⊢ (𝑎 = 𝐶 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝐶) ≠ (𝐵‘𝐶))) |
21 | 20 | elrab 3331 |
. . . . . 6
⊢ (𝐶 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (𝐶 ∈ On ∧ (𝐴‘𝐶) ≠ (𝐵‘𝐶))) |
22 | 21 | notbii 309 |
. . . . 5
⊢ (¬
𝐶 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ (𝐶 ∈ On ∧ (𝐴‘𝐶) ≠ (𝐵‘𝐶))) |
23 | 17, 22 | syl6ib 240 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐶 ∈ On ∧ (𝐴‘𝐶) ≠ (𝐵‘𝐶)))) |
24 | | imnan 437 |
. . . 4
⊢ ((𝐶 ∈ On → ¬ (𝐴‘𝐶) ≠ (𝐵‘𝐶)) ↔ ¬ (𝐶 ∈ On ∧ (𝐴‘𝐶) ≠ (𝐵‘𝐶))) |
25 | 23, 24 | syl6ibr 241 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐶 ∈ On → ¬ (𝐴‘𝐶) ≠ (𝐵‘𝐶)))) |
26 | 5, 25 | mpdd 42 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝐶) ≠ (𝐵‘𝐶))) |
27 | | df-ne 2782 |
. . 3
⊢ ((𝐴‘𝐶) ≠ (𝐵‘𝐶) ↔ ¬ (𝐴‘𝐶) = (𝐵‘𝐶)) |
28 | 27 | con2bii 346 |
. 2
⊢ ((𝐴‘𝐶) = (𝐵‘𝐶) ↔ ¬ (𝐴‘𝐶) ≠ (𝐵‘𝐶)) |
29 | 26, 28 | syl6ibr 241 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐶 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝐶) = (𝐵‘𝐶))) |