Step | Hyp | Ref
| Expression |
1 | | sltirr 31069 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → ¬ 𝐴
<s 𝐴) |
2 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐴 <s 𝐴 ↔ 𝐴 <s 𝐵)) |
3 | 2 | notbid 307 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (¬ 𝐴 <s 𝐴 ↔ ¬ 𝐴 <s 𝐵)) |
4 | 1, 3 | syl5ibcom 234 |
. . . . . . . 8
⊢ (𝐴 ∈
No → (𝐴 =
𝐵 → ¬ 𝐴 <s 𝐵)) |
5 | 4 | con2d 128 |
. . . . . . 7
⊢ (𝐴 ∈
No → (𝐴 <s
𝐵 → ¬ 𝐴 = 𝐵)) |
6 | 5 | imp 444 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐴 <s
𝐵) → ¬ 𝐴 = 𝐵) |
7 | 6 | ad2ant2rl 781 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵)) → ¬ 𝐴 = 𝐵) |
8 | | nofun 31046 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → Fun 𝐴) |
9 | | nofun 31046 |
. . . . . . . . 9
⊢ (𝐵 ∈
No → Fun 𝐵) |
10 | | eqfunfv 6224 |
. . . . . . . . 9
⊢ ((Fun
𝐴 ∧ Fun 𝐵) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
11 | 8, 9, 10 | syl2an 493 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 = 𝐵 ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
12 | 11 | notbid 307 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ 𝐴 = 𝐵 ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵)) → (¬ 𝐴 = 𝐵 ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)))) |
14 | | imnan 437 |
. . . . . . . . . . . 12
⊢ ((dom
𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) ↔ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) |
15 | 14 | biimpri 217 |
. . . . . . . . . . 11
⊢ (¬
(dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) → (dom 𝐴 = dom 𝐵 → ¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) |
16 | 15 | impcom 445 |
. . . . . . . . . 10
⊢ ((dom
𝐴 = dom 𝐵 ∧ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) → ¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) |
17 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
18 | 17 | rexbii 3023 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈ dom
𝐴(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ∃𝑥 ∈ dom 𝐴 ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
19 | | rexnal 2978 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈ dom
𝐴 ¬ (𝐴‘𝑥) = (𝐵‘𝑥) ↔ ¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) |
20 | 18, 19 | bitri 263 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ dom
𝐴(𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) |
21 | | nodenselem4 31083 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
22 | | eloni 5650 |
. . . . . . . . . . . . . . 15
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → Ord ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → Ord ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
24 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → Ord ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
25 | | nodmord 31050 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈
No → Ord dom 𝐴) |
26 | 25 | ad3antrrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → Ord dom 𝐴) |
27 | | nodmon 31047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
28 | | onelon 5665 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((dom
𝐴 ∈ On ∧ 𝑥 ∈ dom 𝐴) → 𝑥 ∈ On) |
29 | 27, 28 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
dom 𝐴) → 𝑥 ∈ On) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈
No → (𝑥 ∈
dom 𝐴 → 𝑥 ∈ On)) |
31 | 30 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ On)) |
32 | 31 | anim1d 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ((𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → (𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)))) |
33 | 32 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → (𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
34 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝐴‘𝑎) = (𝐴‘𝑥)) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝐵‘𝑎) = (𝐵‘𝑥)) |
36 | 34, 35 | neeq12d 2843 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
37 | 36 | intminss 4438 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥) |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥) |
39 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → 𝑥 ∈ dom 𝐴) |
40 | | ordtr2 5685 |
. . . . . . . . . . . . . 14
⊢ ((Ord
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∧ Ord dom 𝐴) → ((∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝐴) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
41 | 40 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((Ord
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∧ Ord dom 𝐴) ∧ (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥 ∧ 𝑥 ∈ dom 𝐴)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴) |
42 | 24, 26, 38, 39, 41 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) ∧ (𝑥 ∈ dom 𝐴 ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴) |
43 | 42 | rexlimdvaa 3014 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → (∃𝑥 ∈ dom 𝐴(𝐴‘𝑥) ≠ (𝐵‘𝑥) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
44 | 20, 43 | syl5bir 232 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → (¬ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
45 | 16, 44 | syl5 33 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 <s 𝐵) → ((dom 𝐴 = dom 𝐵 ∧ ¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥))) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
46 | 45 | exp4b 630 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (dom 𝐴 = dom 𝐵 → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)))) |
47 | 46 | com23 84 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (dom 𝐴 = dom 𝐵 → (𝐴 <s 𝐵 → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)))) |
48 | 47 | imp32 448 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵)) → (¬ (dom 𝐴 = dom 𝐵 ∧ ∀𝑥 ∈ dom 𝐴(𝐴‘𝑥) = (𝐵‘𝑥)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
49 | 13, 48 | sylbid 229 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵)) → (¬ 𝐴 = 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
50 | 7, 49 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴) |
51 | 50 | ex 449 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
52 | | bdayval 31045 |
. . . . 5
⊢ (𝐴 ∈
No → ( bday ‘𝐴) = dom 𝐴) |
53 | | bdayval 31045 |
. . . . 5
⊢ (𝐵 ∈
No → ( bday ‘𝐵) = dom 𝐵) |
54 | 52, 53 | eqeqan12d 2626 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( bday
‘𝐴) = ( bday ‘𝐵) ↔ dom 𝐴 = dom 𝐵)) |
55 | 54 | anbi1d 737 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵) ↔ (dom 𝐴 = dom 𝐵 ∧ 𝐴 <s 𝐵))) |
56 | 52 | eleq2d 2673 |
. . . 4
⊢ (𝐴 ∈
No → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴) ↔
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
57 | 56 | adantr 480 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴) ↔
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ dom 𝐴)) |
58 | 51, 55, 57 | 3imtr4d 282 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴))) |
59 | 58 | imp 444 |
1
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday
‘𝐴)) |