Step | Hyp | Ref
| Expression |
1 | | nodenselem4 31083 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
2 | 1 | adantrl 748 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
3 | | nofnbday 31049 |
. . . . . 6
⊢ (𝐴 ∈
No → 𝐴 Fn
( bday ‘𝐴)) |
4 | 3 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 Fn ( bday
‘𝐴)) |
5 | | nodenselem5 31084 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴)) |
6 | | bdayelon 31079 |
. . . . . . 7
⊢ ( bday ‘𝐴) ∈ On |
7 | 6 | onelssi 5753 |
. . . . . 6
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴) →
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ ( bday
‘𝐴)) |
8 | 5, 7 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ ( bday
‘𝐴)) |
9 | | fnssres 5918 |
. . . . 5
⊢ ((𝐴 Fn ( bday
‘𝐴) ∧
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ ( bday
‘𝐴)) →
(𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) Fn ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
10 | 4, 8, 9 | syl2anc 691 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) Fn ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
11 | | resss 5342 |
. . . . . 6
⊢ (𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ 𝐴 |
12 | | rnss 5275 |
. . . . . 6
⊢ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ 𝐴 → ran (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ ran 𝐴) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
⊢ ran
(𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ ran 𝐴 |
14 | | norn 31048 |
. . . . . 6
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1𝑜, 2𝑜}) |
15 | 14 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ran 𝐴 ⊆ {1𝑜,
2𝑜}) |
16 | 13, 15 | syl5ss 3579 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ran (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ {1𝑜,
2𝑜}) |
17 | | df-f 5808 |
. . . 4
⊢ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}⟶{1𝑜,
2𝑜} ↔ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) Fn ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∧ ran (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ⊆ {1𝑜,
2𝑜})) |
18 | 10, 16, 17 | sylanbrc 695 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}⟶{1𝑜,
2𝑜}) |
19 | | feq2 5940 |
. . . 4
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):𝑥⟶{1𝑜,
2𝑜} ↔ (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}⟶{1𝑜,
2𝑜})) |
20 | 19 | rspcev 3282 |
. . 3
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}⟶{1𝑜,
2𝑜}) → ∃𝑥 ∈ On (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):𝑥⟶{1𝑜,
2𝑜}) |
21 | 2, 18, 20 | syl2anc 691 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ On (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):𝑥⟶{1𝑜,
2𝑜}) |
22 | | elno 31043 |
. 2
⊢ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
↔ ∃𝑥 ∈ On
(𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}):𝑥⟶{1𝑜,
2𝑜}) |
23 | 21, 22 | sylibr 223 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
) |