Step | Hyp | Ref
| Expression |
1 | | nodenselem6 31085 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
) |
2 | | bdayval 31045 |
. . . . 5
⊢ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
→ ( bday ‘(𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) = dom (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) = dom (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
4 | | dmres 5339 |
. . . . 5
⊢ dom
(𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∩ dom 𝐴) |
5 | | nodenselem5 31084 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴)) |
6 | | bdayelon 31079 |
. . . . . . . . 9
⊢ ( bday ‘𝐴) ∈ On |
7 | 6 | onelssi 5753 |
. . . . . . . 8
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴) →
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ ( bday
‘𝐴)) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ ( bday
‘𝐴)) |
9 | | bdayval 31045 |
. . . . . . . 8
⊢ (𝐴 ∈
No → ( bday ‘𝐴) = dom 𝐴) |
10 | 9 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘𝐴) = dom
𝐴) |
11 | 8, 10 | sseqtrd 3604 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ dom 𝐴) |
12 | | df-ss 3554 |
. . . . . 6
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ dom 𝐴 ↔ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∩ dom 𝐴) = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
13 | 11, 12 | sylib 207 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∩ dom 𝐴) = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
14 | 4, 13 | syl5eq 2656 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → dom (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
15 | 3, 14 | eqtrd 2644 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
16 | 15, 5 | eqeltrd 2688 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ∈ ( bday
‘𝐴)) |
17 | | nodenselem4 31083 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
18 | 17 | adantrl 748 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
19 | | nodenselem8 31087 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 <s 𝐵 ↔ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜))) |
20 | 19 | biimpd 218 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ ( bday
‘𝐴) = ( bday ‘𝐵)) → (𝐴 <s 𝐵 → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜))) |
21 | 20 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) = ( bday ‘𝐵) → (𝐴 <s 𝐵 → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜)))) |
22 | 21 | imp32 448 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜)) |
23 | 22 | simpld 474 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜) |
24 | | eqid 2610 |
. . . . . . . . 9
⊢ ∅ =
∅ |
25 | 23, 24 | jctir 559 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ ∅ =
∅)) |
26 | 25 | 3mix1d 1229 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ ∅ =
∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ ∅ =
2𝑜) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ ∅ =
2𝑜))) |
27 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
28 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
29 | 27, 28 | brtp 30892 |
. . . . . . 7
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}∅ ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ ∅ =
∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1𝑜 ∧ ∅ =
2𝑜) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ ∅ =
2𝑜))) |
30 | 26, 29 | sylibr 223 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉}∅) |
31 | 15 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
32 | | fvnobday 31081 |
. . . . . . . 8
⊢ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
→ ((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) = ∅) |
33 | 1, 32 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) = ∅) |
34 | 31, 33 | eqtr3d 2646 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
35 | 30, 34 | breqtrrd 4611 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
36 | | fvres 6117 |
. . . . . . 7
⊢ (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐴‘𝑦)) |
37 | 36 | eqcomd 2616 |
. . . . . 6
⊢ (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦)) |
38 | 37 | rgen 2906 |
. . . . 5
⊢
∀𝑦 ∈
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) |
39 | 35, 38 | jctil 558 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
40 | | raleq 3115 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦))) |
41 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
42 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
43 | 41, 42 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
44 | 40, 43 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
45 | 44 | rspcev 3282 |
. . . 4
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥))) |
46 | 18, 39, 45 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥))) |
47 | | simpll 786 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 ∈ No
) |
48 | | sltval 31044 |
. . . 4
⊢ ((𝐴 ∈
No ∧ (𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No )
→ (𝐴 <s (𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥)))) |
49 | 47, 1, 48 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 <s (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) ∧ (𝐴‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥)))) |
50 | 46, 49 | mpbird 246 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐴 <s (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
51 | 37 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴‘𝑦) = ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦)) |
52 | | nodenselem7 31086 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐵‘𝑦))) |
53 | 52 | imp 444 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴‘𝑦) = (𝐵‘𝑦)) |
54 | 51, 53 | eqtr3d 2646 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦)) |
55 | 54 | ralrimiva 2949 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦)) |
56 | 22 | simprd 478 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) |
57 | 56, 24 | jctil 558 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (∅ = ∅ ∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜)) |
58 | 57 | 3mix3d 1231 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((∅ = 1𝑜
∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ (∅ =
1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ (∅ =
∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜))) |
59 | | fvex 6113 |
. . . . . . 7
⊢ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
60 | 28, 59 | brtp 30892 |
. . . . . 6
⊢
(∅{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ((∅ = 1𝑜
∧ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ (∅ =
1𝑜 ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2𝑜) ∨ (∅ =
∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) =
2𝑜))) |
61 | 58, 60 | sylibr 223 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) →
∅{〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
62 | 34, 61 | eqbrtrd 4605 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
63 | | raleq 3115 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦))) |
64 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
65 | 42, 64 | breq12d 4596 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥) ↔ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
66 | 63, 65 | anbi12d 743 |
. . . . 5
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
67 | 66 | rspcev 3282 |
. . . 4
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥))) |
68 | 18, 55, 62, 67 | syl12anc 1316 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥))) |
69 | | simplr 788 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → 𝐵 ∈ No
) |
70 | | sltval 31044 |
. . . 4
⊢ (((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
∧ 𝐵 ∈ No ) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥)))) |
71 | 1, 69, 70 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑦) = (𝐵‘𝑦) ∧ ((𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})‘𝑥){〈1𝑜, ∅〉,
〈1𝑜, 2𝑜〉, 〈∅,
2𝑜〉} (𝐵‘𝑥)))) |
72 | 68, 71 | mpbird 246 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵) |
73 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ( bday
‘𝑥) = ( bday ‘(𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
74 | 73 | eleq1d 2672 |
. . . 4
⊢ (𝑥 = (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (( bday
‘𝑥) ∈
( bday ‘𝐴) ↔ ( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ∈ ( bday
‘𝐴))) |
75 | | breq2 4587 |
. . . 4
⊢ (𝑥 = (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴 <s 𝑥 ↔ 𝐴 <s (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
76 | | breq1 4586 |
. . . 4
⊢ (𝑥 = (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝑥 <s 𝐵 ↔ (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵)) |
77 | 74, 75, 76 | 3anbi123d 1391 |
. . 3
⊢ (𝑥 = (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ((( bday
‘𝑥) ∈
( bday ‘𝐴) ∧ 𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵) ↔ (( bday
‘(𝐴 ↾
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ∈ ( bday
‘𝐴) ∧
𝐴 <s (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∧ (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵))) |
78 | 77 | rspcev 3282 |
. 2
⊢ (((𝐴 ↾ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ No
∧ (( bday ‘(𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ∈ ( bday
‘𝐴) ∧
𝐴 <s (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∧ (𝐴 ↾ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) <s 𝐵)) → ∃𝑥 ∈ No
(( bday ‘𝑥) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵)) |
79 | 1, 16, 50, 72, 78 | syl13anc 1320 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑥 ∈ No
(( bday ‘𝑥) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑥 ∧ 𝑥 <s 𝐵)) |