Step | Hyp | Ref
| Expression |
1 | | sltval 33620 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) |
2 | | fvex 6751 |
. . . . . . . . . . . . 13
⊢ (𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
3 | | fvex 6751 |
. . . . . . . . . . . . 13
⊢ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ∈ V |
4 | 2, 3 | brtp 33466 |
. . . . . . . . . . . 12
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ (((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o))) |
5 | | 1n0 8244 |
. . . . . . . . . . . . . . . . 17
⊢
1o ≠ ∅ |
6 | 5 | neii 2945 |
. . . . . . . . . . . . . . . 16
⊢ ¬
1o = ∅ |
7 | | eqeq1 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 1o =
∅)) |
8 | 6, 7 | mtbiri 330 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ¬ (𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
9 | | fvprc 6730 |
. . . . . . . . . . . . . . 15
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
10 | 8, 9 | nsyl2 143 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
11 | 10 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
12 | 10 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
13 | | 2on0 8234 |
. . . . . . . . . . . . . . . . 17
⊢
2o ≠ ∅ |
14 | 13 | neii 2945 |
. . . . . . . . . . . . . . . 16
⊢ ¬
2o = ∅ |
15 | | eqeq1 2743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ↔ 2o =
∅)) |
16 | 14, 15 | mtbiri 330 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ¬ (𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
17 | | fvprc 6730 |
. . . . . . . . . . . . . . 15
⊢ (¬
∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V → (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) |
18 | 16, 17 | nsyl2 143 |
. . . . . . . . . . . . . 14
⊢ ((𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
19 | 18 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
20 | 11, 12, 19 | 3jaoi 1429 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 1o ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o) ∨ ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = ∅ ∧ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = 2o)) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
21 | 4, 20 | sylbi 220 |
. . . . . . . . . . 11
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V) |
22 | | onintrab 7601 |
. . . . . . . . . . 11
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V ↔ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
23 | 21, 22 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
24 | 23 | adantl 485 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
25 | | onelon 6258 |
. . . . . . . . . . . . . 14
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ 𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑦 ∈ On) |
26 | 25 | expcom 417 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On → 𝑦 ∈ On)) |
27 | 24, 26 | syl5 34 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (((𝐴 ∈ No
∧ 𝐵 ∈ No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → 𝑦 ∈ On)) |
28 | | fveq2 6738 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → (𝐴‘𝑎) = (𝐴‘𝑦)) |
29 | | fveq2 6738 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → (𝐵‘𝑎) = (𝐵‘𝑦)) |
30 | 28, 29 | neeq12d 3005 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑦 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑦) ≠ (𝐵‘𝑦))) |
31 | 30 | onnminsb 7604 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ On → (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦))) |
32 | 31 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝑦 ∈ On → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦))) |
33 | 27, 32 | syldc 48 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦))) |
34 | | df-ne 2944 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑦) ≠ (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) = (𝐵‘𝑦)) |
35 | 34 | con2bii 361 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ ¬ (𝐴‘𝑦) ≠ (𝐵‘𝑦)) |
36 | 33, 35 | syl6ibr 255 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐵‘𝑦))) |
37 | 36 | ralrimiv 3107 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) |
38 | 24, 37 | jca 515 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))) |
39 | 38 | ex 416 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)))) |
40 | 39 | impac 556 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ((∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
41 | | anass 472 |
. . . . . 6
⊢ (((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) ↔ (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
42 | 40, 41 | sylib 221 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
43 | | raleq 3334 |
. . . . . . 7
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ↔ ∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦))) |
44 | | fveq2 6738 |
. . . . . . . 8
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
45 | | fveq2 6738 |
. . . . . . . 8
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
46 | 44, 45 | breq12d 5082 |
. . . . . . 7
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
47 | 43, 46 | anbi12d 634 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) ↔ (∀𝑦 ∈ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
48 | 47 | rspcev 3552 |
. . . . 5
⊢ ((∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (∀𝑦 ∈ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
49 | 42, 48 | syl 17 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥))) |
50 | 49 | ex 416 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) |
51 | | eqeq12 2756 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1o =
∅)) |
52 | 6, 51 | mtbiri 330 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
53 | | 1on 8232 |
. . . . . . . . . . . . . . . . 17
⊢
1o ∈ On |
54 | | 0elon 6286 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
∈ On |
55 | | suc11 6336 |
. . . . . . . . . . . . . . . . . 18
⊢
((1o ∈ On ∧ ∅ ∈ On) → (suc
1o = suc ∅ ↔ 1o = ∅)) |
56 | 55 | necon3bid 2988 |
. . . . . . . . . . . . . . . . 17
⊢
((1o ∈ On ∧ ∅ ∈ On) → (suc
1o ≠ suc ∅ ↔ 1o ≠
∅)) |
57 | 53, 54, 56 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (suc
1o ≠ suc ∅ ↔ 1o ≠
∅) |
58 | 5, 57 | mpbir 234 |
. . . . . . . . . . . . . . 15
⊢ suc
1o ≠ suc ∅ |
59 | | df-2o 8226 |
. . . . . . . . . . . . . . . 16
⊢
2o = suc 1o |
60 | | df-1o 8225 |
. . . . . . . . . . . . . . . 16
⊢
1o = suc ∅ |
61 | 59, 60 | eqeq12i 2757 |
. . . . . . . . . . . . . . 15
⊢
(2o = 1o ↔ suc 1o = suc
∅) |
62 | 58, 61 | nemtbir 3040 |
. . . . . . . . . . . . . 14
⊢ ¬
2o = 1o |
63 | | eqeq12 2756 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 1o =
2o)) |
64 | | eqcom 2746 |
. . . . . . . . . . . . . . 15
⊢
(1o = 2o ↔ 2o =
1o) |
65 | 63, 64 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ 2o =
1o)) |
66 | 62, 65 | mtbiri 330 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
67 | 13 | nesymi 3001 |
. . . . . . . . . . . . . 14
⊢ ¬
∅ = 2o |
68 | | eqeq12 2756 |
. . . . . . . . . . . . . 14
⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o) → ((𝐴‘𝑥) = (𝐵‘𝑥) ↔ ∅ =
2o)) |
69 | 67, 68 | mtbiri 330 |
. . . . . . . . . . . . 13
⊢ (((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
70 | 52, 66, 69 | 3jaoi 1429 |
. . . . . . . . . . . 12
⊢ ((((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o)) → ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
71 | | fvex 6751 |
. . . . . . . . . . . . 13
⊢ (𝐴‘𝑥) ∈ V |
72 | | fvex 6751 |
. . . . . . . . . . . . 13
⊢ (𝐵‘𝑥) ∈ V |
73 | 71, 72 | brtp 33466 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = ∅) ∨ ((𝐴‘𝑥) = 1o ∧ (𝐵‘𝑥) = 2o) ∨ ((𝐴‘𝑥) = ∅ ∧ (𝐵‘𝑥) = 2o))) |
74 | | df-ne 2944 |
. . . . . . . . . . . 12
⊢ ((𝐴‘𝑥) ≠ (𝐵‘𝑥) ↔ ¬ (𝐴‘𝑥) = (𝐵‘𝑥)) |
75 | 70, 73, 74 | 3imtr4i 295 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) → (𝐴‘𝑥) ≠ (𝐵‘𝑥)) |
76 | | fveq2 6738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝐴‘𝑎) = (𝐴‘𝑥)) |
77 | | fveq2 6738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → (𝐵‘𝑎) = (𝐵‘𝑥)) |
78 | 76, 77 | neeq12d 3005 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑥 → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
79 | 78 | elrab 3617 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥))) |
80 | 79 | biimpri 231 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
81 | 80 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
82 | | ssrab2 4009 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On |
83 | | ne0i 4265 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) |
84 | 83 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) |
85 | | onint 7595 |
. . . . . . . . . . . . . . . . . 18
⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
86 | 82, 84, 85 | sylancr 590 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
87 | | nfrab1 3311 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} |
88 | 87 | nfint 4885 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑎∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} |
89 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑎On |
90 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎𝐴 |
91 | 90, 88 | nffv 6748 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎(𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
92 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑎𝐵 |
93 | 92, 88 | nffv 6748 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑎(𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
94 | 91, 93 | nfne 3045 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑎(𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
95 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑎) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
96 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑎) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
97 | 95, 96 | neeq12d 3005 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑎) ≠ (𝐵‘𝑎) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
98 | 88, 89, 94, 97 | elrabf 3613 |
. . . . . . . . . . . . . . . . . 18
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On ∧ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
99 | 98 | simprbi 500 |
. . . . . . . . . . . . . . . . 17
⊢ (∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
100 | 86, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
101 | | df-ne 2944 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ≠ (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
102 | 100, 101 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
103 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐴‘𝑦) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
104 | | fveq2 6738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → (𝐵‘𝑦) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
105 | 103, 104 | eqeq12d 2755 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ((𝐴‘𝑦) = (𝐵‘𝑦) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
106 | 105 | rspccv 3549 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) → (∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
107 | 106 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥 → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
108 | 102, 107 | mtod 201 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥) |
109 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ∈ On) |
110 | | oninton 7600 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ≠ ∅) → ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
111 | 82, 83, 110 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
112 | 111 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) |
113 | | ontri1 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ ∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥)) |
114 | 109, 112,
113 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → (𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ↔ ¬ ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ 𝑥)) |
115 | 108, 114 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 ⊆ ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
116 | | intss1 4890 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥) |
117 | 116 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → ∩
{𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ⊆ 𝑥) |
118 | 115, 117 | eqssd 3934 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
119 | 81, 118 | syldan 594 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥) ≠ (𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
120 | 75, 119 | sylan2 596 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → 𝑥 = ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) |
121 | 120 | fveq2d 6742 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → (𝐴‘𝑥) = (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
122 | 120 | fveq2d 6742 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → (𝐵‘𝑥) = (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
123 | 121, 122 | breq12d 5082 |
. . . . . . . 8
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
124 | 123 | biimpd 232 |
. . . . . . 7
⊢ (((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
125 | 124 | ex 416 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))) |
126 | 125 | pm2.43d 53 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦)) → ((𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
127 | 126 | expimpd 457 |
. . . 4
⊢ (𝑥 ∈ On →
((∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |
128 | 127 | rexlimiv 3209 |
. . 3
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)) → (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})) |
129 | 50, 128 | impbid1 228 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘𝑥)))) |
130 | 1, 129 | bitr4d 285 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){〈1o, ∅〉,
〈1o, 2o〉, 〈∅, 2o〉}
(𝐵‘∩ {𝑎
∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}))) |