Step | Hyp | Ref
| Expression |
1 | | wepwso.f |
. . 3
⊢ 𝐹 = (𝑎 ∈ (2o ↑m
𝐴) ↦ (◡𝑎 “ {1o})) |
2 | 1 | pw2f1o2 40432 |
. 2
⊢ (𝐴 ∈ V → 𝐹:(2o
↑m 𝐴)–1-1-onto→𝒫 𝐴) |
3 | | fvex 6687 |
. . . . . . . 8
⊢ (𝑐‘𝑧) ∈ V |
4 | 3 | epeli 5436 |
. . . . . . 7
⊢ ((𝑏‘𝑧) E (𝑐‘𝑧) ↔ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) |
5 | | elmapi 8459 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (2o
↑m 𝐴)
→ 𝑏:𝐴⟶2o) |
6 | 5 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
→ 𝑏:𝐴⟶2o) |
7 | 6 | ffvelrnda 6861 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (𝑏‘𝑧) ∈ 2o) |
8 | | elmapi 8459 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (2o
↑m 𝐴)
→ 𝑐:𝐴⟶2o) |
9 | 8 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
→ 𝑐:𝐴⟶2o) |
10 | 9 | ffvelrnda 6861 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (𝑐‘𝑧) ∈ 2o) |
11 | | n0i 4222 |
. . . . . . . . . . . . 13
⊢ ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → ¬ (𝑐‘𝑧) = ∅) |
12 | 11 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ¬ (𝑐‘𝑧) = ∅) |
13 | | elpri 4538 |
. . . . . . . . . . . . . 14
⊢ ((𝑐‘𝑧) ∈ {∅, 1o} →
((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1o)) |
14 | | df2o3 8146 |
. . . . . . . . . . . . . 14
⊢
2o = {∅, 1o} |
15 | 13, 14 | eleq2s 2851 |
. . . . . . . . . . . . 13
⊢ ((𝑐‘𝑧) ∈ 2o → ((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1o)) |
16 | 15 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1o)) |
17 | | orel1 888 |
. . . . . . . . . . . 12
⊢ (¬
(𝑐‘𝑧) = ∅ → (((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1o) → (𝑐‘𝑧) = 1o)) |
18 | 12, 16, 17 | sylc 65 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → (𝑐‘𝑧) = 1o) |
19 | | 1on 8138 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
20 | 19 | onirri 6279 |
. . . . . . . . . . . . 13
⊢ ¬
1o ∈ 1o |
21 | | eleq12 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏‘𝑧) = 1o ∧ (𝑐‘𝑧) = 1o) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ 1o ∈
1o)) |
22 | 21 | biimpd 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏‘𝑧) = 1o ∧ (𝑐‘𝑧) = 1o) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → 1o ∈
1o)) |
23 | 22 | expcom 417 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐‘𝑧) = 1o → ((𝑏‘𝑧) = 1o → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → 1o ∈
1o))) |
24 | 23 | com3r 87 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → ((𝑐‘𝑧) = 1o → ((𝑏‘𝑧) = 1o → 1o ∈
1o))) |
25 | 24 | imp 410 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘𝑧) ∈ (𝑐‘𝑧) ∧ (𝑐‘𝑧) = 1o) → ((𝑏‘𝑧) = 1o → 1o ∈
1o)) |
26 | 25 | adantll 714 |
. . . . . . . . . . . . 13
⊢
(((((𝑏‘𝑧) ∈ 2o ∧
(𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) ∧ (𝑐‘𝑧) = 1o) → ((𝑏‘𝑧) = 1o → 1o ∈
1o)) |
27 | 20, 26 | mtoi 202 |
. . . . . . . . . . . 12
⊢
(((((𝑏‘𝑧) ∈ 2o ∧
(𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) ∧ (𝑐‘𝑧) = 1o) → ¬ (𝑏‘𝑧) = 1o) |
28 | 18, 27 | mpdan 687 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ¬ (𝑏‘𝑧) = 1o) |
29 | 18, 28 | jca 515 |
. . . . . . . . . 10
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o)) |
30 | | elpri 4538 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑧) ∈ {∅, 1o} →
((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1o)) |
31 | 30, 14 | eleq2s 2851 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑧) ∈ 2o → ((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1o)) |
32 | 31 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) → ((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1o)) |
33 | | orel2 890 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑏‘𝑧) = 1o → (((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1o) → (𝑏‘𝑧) = ∅)) |
34 | 32, 33 | mpan9 510 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ ¬ (𝑏‘𝑧) = 1o) → (𝑏‘𝑧) = ∅) |
35 | 34 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o)) → (𝑏‘𝑧) = ∅) |
36 | | 0lt1o 8160 |
. . . . . . . . . . . 12
⊢ ∅
∈ 1o |
37 | 35, 36 | eqeltrdi 2841 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o)) → (𝑏‘𝑧) ∈ 1o) |
38 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o)) → (𝑐‘𝑧) = 1o) |
39 | 37, 38 | eleqtrrd 2836 |
. . . . . . . . . 10
⊢ ((((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) ∧ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o)) → (𝑏‘𝑧) ∈ (𝑐‘𝑧)) |
40 | 29, 39 | impbida 801 |
. . . . . . . . 9
⊢ (((𝑏‘𝑧) ∈ 2o ∧ (𝑐‘𝑧) ∈ 2o) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o))) |
41 | 7, 10, 40 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o))) |
42 | | simplrr 778 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → 𝑐 ∈ (2o ↑m
𝐴)) |
43 | 1 | pw2f1o2val2 40434 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (2o
↑m 𝐴) ∧
𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑧) = 1o)) |
44 | 42, 43 | sylancom 591 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑧) = 1o)) |
45 | | simplrl 777 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → 𝑏 ∈ (2o ↑m
𝐴)) |
46 | 1 | pw2f1o2val2 40434 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (2o
↑m 𝐴) ∧
𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑧) = 1o)) |
47 | 45, 46 | sylancom 591 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑧) = 1o)) |
48 | 47 | notbid 321 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (¬ 𝑧 ∈ (𝐹‘𝑏) ↔ ¬ (𝑏‘𝑧) = 1o)) |
49 | 44, 48 | anbi12d 634 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ↔ ((𝑐‘𝑧) = 1o ∧ ¬ (𝑏‘𝑧) = 1o))) |
50 | 41, 49 | bitr4d 285 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
51 | 4, 50 | syl5bb 286 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) E (𝑐‘𝑧) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
52 | 6 | ffvelrnda 6861 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → (𝑏‘𝑤) ∈ 2o) |
53 | 9 | ffvelrnda 6861 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → (𝑐‘𝑤) ∈ 2o) |
54 | | eqeq1 2742 |
. . . . . . . . . . . 12
⊢ ((𝑏‘𝑤) = (𝑐‘𝑤) → ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) |
55 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑏‘𝑤) = ∅) |
56 | | 1n0 8150 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1o ≠ ∅ |
57 | 56 | nesymi 2991 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
∅ = 1o |
58 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏‘𝑤) = ∅ → ((𝑏‘𝑤) = 1o ↔ ∅ =
1o)) |
59 | 57, 58 | mtbiri 330 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏‘𝑤) = ∅ → ¬ (𝑏‘𝑤) = 1o) |
60 | 59 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → ¬ (𝑏‘𝑤) = 1o) |
61 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) |
62 | 60, 61 | mtbid 327 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → ¬ (𝑐‘𝑤) = 1o) |
63 | | elpri 4538 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐‘𝑤) ∈ {∅, 1o} →
((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1o)) |
64 | 63, 14 | eleq2s 2851 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐‘𝑤) ∈ 2o → ((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1o)) |
65 | 64 | ad3antlr 731 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → ((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1o)) |
66 | | orel2 890 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑐‘𝑤) = 1o → (((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1o) → (𝑐‘𝑤) = ∅)) |
67 | 62, 65, 66 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑐‘𝑤) = ∅) |
68 | 55, 67 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑏‘𝑤) = (𝑐‘𝑤)) |
69 | 68 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑤) ∈ 2o ∧ (𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = ∅) → (((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
70 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = 1o) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑏‘𝑤) = 1o) |
71 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = 1o) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) |
72 | 70, 71 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = 1o) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑐‘𝑤) = 1o) |
73 | 70, 72 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
⊢
(((((𝑏‘𝑤) ∈ 2o ∧
(𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = 1o) ∧ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o)) → (𝑏‘𝑤) = (𝑐‘𝑤)) |
74 | 73 | ex 416 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑤) ∈ 2o ∧ (𝑐‘𝑤) ∈ 2o) ∧ (𝑏‘𝑤) = 1o) → (((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
75 | | elpri 4538 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑤) ∈ {∅, 1o} →
((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1o)) |
76 | 75, 14 | eleq2s 2851 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑤) ∈ 2o → ((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1o)) |
77 | 76 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘𝑤) ∈ 2o ∧ (𝑐‘𝑤) ∈ 2o) → ((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1o)) |
78 | 69, 74, 77 | mpjaodan 958 |
. . . . . . . . . . . 12
⊢ (((𝑏‘𝑤) ∈ 2o ∧ (𝑐‘𝑤) ∈ 2o) → (((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
79 | 54, 78 | impbid2 229 |
. . . . . . . . . . 11
⊢ (((𝑏‘𝑤) ∈ 2o ∧ (𝑐‘𝑤) ∈ 2o) → ((𝑏‘𝑤) = (𝑐‘𝑤) ↔ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o))) |
80 | 52, 53, 79 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → ((𝑏‘𝑤) = (𝑐‘𝑤) ↔ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o))) |
81 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → 𝑏 ∈ (2o ↑m
𝐴)) |
82 | 1 | pw2f1o2val2 40434 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (2o
↑m 𝐴) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑤) = 1o)) |
83 | 81, 82 | sylancom 591 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑤) = 1o)) |
84 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → 𝑐 ∈ (2o ↑m
𝐴)) |
85 | 1 | pw2f1o2val2 40434 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ (2o
↑m 𝐴) ∧
𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑤) = 1o)) |
86 | 84, 85 | sylancom 591 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑤) = 1o)) |
87 | 83, 86 | bibi12d 349 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → ((𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)) ↔ ((𝑏‘𝑤) = 1o ↔ (𝑐‘𝑤) = 1o))) |
88 | 80, 87 | bitr4d 285 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → ((𝑏‘𝑤) = (𝑐‘𝑤) ↔ (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))) |
89 | 88 | imbi2d 344 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑤 ∈ 𝐴) → ((𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
90 | 89 | ralbidva 3108 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
→ (∀𝑤 ∈
𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
91 | 90 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
92 | 51, 91 | anbi12d 634 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
∧ 𝑧 ∈ 𝐴) → (((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))) ↔ ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
93 | 92 | rexbidva 3206 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
→ (∃𝑧 ∈
𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
94 | | vex 3402 |
. . . . 5
⊢ 𝑏 ∈ V |
95 | | vex 3402 |
. . . . 5
⊢ 𝑐 ∈ V |
96 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥‘𝑧) = (𝑏‘𝑧)) |
97 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑦 = 𝑐 → (𝑦‘𝑧) = (𝑐‘𝑧)) |
98 | 96, 97 | breqan12d 5046 |
. . . . . . 7
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑥‘𝑧) E (𝑦‘𝑧) ↔ (𝑏‘𝑧) E (𝑐‘𝑧))) |
99 | | fveq1 6673 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑥‘𝑤) = (𝑏‘𝑤)) |
100 | | fveq1 6673 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑐 → (𝑦‘𝑤) = (𝑐‘𝑤)) |
101 | 99, 100 | eqeqan12d 2755 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑏‘𝑤) = (𝑐‘𝑤))) |
102 | 101 | imbi2d 344 |
. . . . . . . 8
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
103 | 102 | ralbidv 3109 |
. . . . . . 7
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
104 | 98, 103 | anbi12d 634 |
. . . . . 6
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))))) |
105 | 104 | rexbidv 3207 |
. . . . 5
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))))) |
106 | | wepwso.u |
. . . . 5
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
107 | 94, 95, 105, 106 | braba 5392 |
. . . 4
⊢ (𝑏𝑈𝑐 ↔ ∃𝑧 ∈ 𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
108 | | fvex 6687 |
. . . . 5
⊢ (𝐹‘𝑏) ∈ V |
109 | | fvex 6687 |
. . . . 5
⊢ (𝐹‘𝑐) ∈ V |
110 | | eleq2 2821 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑐) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝐹‘𝑐))) |
111 | | eleq2 2821 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑏) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝐹‘𝑏))) |
112 | 111 | notbid 321 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑏) → (¬ 𝑧 ∈ 𝑥 ↔ ¬ 𝑧 ∈ (𝐹‘𝑏))) |
113 | 110, 112 | bi2anan9r 640 |
. . . . . . 7
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
114 | | eleq2 2821 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑏) → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ (𝐹‘𝑏))) |
115 | | eleq2 2821 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑐) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (𝐹‘𝑐))) |
116 | 114, 115 | bi2bian9 641 |
. . . . . . . . 9
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))) |
117 | 116 | imbi2d 344 |
. . . . . . . 8
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) ↔ (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
118 | 117 | ralbidv 3109 |
. . . . . . 7
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
119 | 113, 118 | anbi12d 634 |
. . . . . 6
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦))) ↔ ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
120 | 119 | rexbidv 3207 |
. . . . 5
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦))) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
121 | | wepwso.t |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))} |
122 | 108, 109,
120, 121 | braba 5392 |
. . . 4
⊢ ((𝐹‘𝑏)𝑇(𝐹‘𝑐) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
123 | 93, 107, 122 | 3bitr4g 317 |
. . 3
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2o
↑m 𝐴) ∧
𝑐 ∈ (2o
↑m 𝐴)))
→ (𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐))) |
124 | 123 | ralrimivva 3103 |
. 2
⊢ (𝐴 ∈ V → ∀𝑏 ∈ (2o
↑m 𝐴)∀𝑐 ∈ (2o ↑m
𝐴)(𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐))) |
125 | | df-isom 6348 |
. 2
⊢ (𝐹 Isom 𝑈, 𝑇 ((2o ↑m 𝐴), 𝒫 𝐴) ↔ (𝐹:(2o ↑m 𝐴)–1-1-onto→𝒫 𝐴 ∧ ∀𝑏 ∈ (2o ↑m
𝐴)∀𝑐 ∈ (2o
↑m 𝐴)(𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐)))) |
126 | 2, 124, 125 | sylanbrc 586 |
1
⊢ (𝐴 ∈ V → 𝐹 Isom 𝑈, 𝑇 ((2o ↑m 𝐴), 𝒫 𝐴)) |