Step | Hyp | Ref
| Expression |
1 | | wepwso.f |
. . 3
⊢ 𝐹 = (𝑎 ∈ (2𝑜
↑𝑚 𝐴) ↦ (◡𝑎 “
{1𝑜})) |
2 | 1 | pw2f1o2 36623 |
. 2
⊢ (𝐴 ∈ V → 𝐹:(2𝑜
↑𝑚 𝐴)–1-1-onto→𝒫 𝐴) |
3 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑐‘𝑧) ∈ V |
4 | 3 | epelc 4951 |
. . . . . . 7
⊢ ((𝑏‘𝑧) E (𝑐‘𝑧) ↔ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) |
5 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) → 𝑏:𝐴⟶2𝑜) |
6 | 5 | ad2antrl 760 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) → 𝑏:𝐴⟶2𝑜) |
7 | 6 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (𝑏‘𝑧) ∈
2𝑜) |
8 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (2𝑜
↑𝑚 𝐴) → 𝑐:𝐴⟶2𝑜) |
9 | 8 | ad2antll 761 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) → 𝑐:𝐴⟶2𝑜) |
10 | 9 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (𝑐‘𝑧) ∈
2𝑜) |
11 | | n0i 3879 |
. . . . . . . . . . . . 13
⊢ ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → ¬ (𝑐‘𝑧) = ∅) |
12 | 11 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ¬ (𝑐‘𝑧) = ∅) |
13 | | elpri 4145 |
. . . . . . . . . . . . . 14
⊢ ((𝑐‘𝑧) ∈ {∅, 1𝑜}
→ ((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1𝑜)) |
14 | | df2o3 7460 |
. . . . . . . . . . . . . 14
⊢
2𝑜 = {∅,
1𝑜} |
15 | 13, 14 | eleq2s 2706 |
. . . . . . . . . . . . 13
⊢ ((𝑐‘𝑧) ∈ 2𝑜 → ((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1𝑜)) |
16 | 15 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1𝑜)) |
17 | | orel1 396 |
. . . . . . . . . . . 12
⊢ (¬
(𝑐‘𝑧) = ∅ → (((𝑐‘𝑧) = ∅ ∨ (𝑐‘𝑧) = 1𝑜) → (𝑐‘𝑧) = 1𝑜)) |
18 | 12, 16, 17 | sylc 63 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → (𝑐‘𝑧) = 1𝑜) |
19 | | 1on 7454 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ On |
20 | 19 | onirri 5751 |
. . . . . . . . . . . . 13
⊢ ¬
1𝑜 ∈ 1𝑜 |
21 | | eleq12 2678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏‘𝑧) = 1𝑜 ∧ (𝑐‘𝑧) = 1𝑜) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ 1𝑜 ∈
1𝑜)) |
22 | 21 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏‘𝑧) = 1𝑜 ∧ (𝑐‘𝑧) = 1𝑜) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → 1𝑜 ∈
1𝑜)) |
23 | 22 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐‘𝑧) = 1𝑜 → ((𝑏‘𝑧) = 1𝑜 → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → 1𝑜 ∈
1𝑜))) |
24 | 23 | com3r 85 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑧) ∈ (𝑐‘𝑧) → ((𝑐‘𝑧) = 1𝑜 → ((𝑏‘𝑧) = 1𝑜 →
1𝑜 ∈ 1𝑜))) |
25 | 24 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘𝑧) ∈ (𝑐‘𝑧) ∧ (𝑐‘𝑧) = 1𝑜) → ((𝑏‘𝑧) = 1𝑜 →
1𝑜 ∈ 1𝑜)) |
26 | 25 | adantll 746 |
. . . . . . . . . . . . 13
⊢
(((((𝑏‘𝑧) ∈ 2𝑜
∧ (𝑐‘𝑧) ∈ 2𝑜)
∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) ∧ (𝑐‘𝑧) = 1𝑜) → ((𝑏‘𝑧) = 1𝑜 →
1𝑜 ∈ 1𝑜)) |
27 | 20, 26 | mtoi 189 |
. . . . . . . . . . . 12
⊢
(((((𝑏‘𝑧) ∈ 2𝑜
∧ (𝑐‘𝑧) ∈ 2𝑜)
∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) ∧ (𝑐‘𝑧) = 1𝑜) → ¬
(𝑏‘𝑧) = 1𝑜) |
28 | 18, 27 | mpdan 699 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ¬ (𝑏‘𝑧) = 1𝑜) |
29 | 18, 28 | jca 553 |
. . . . . . . . . 10
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ (𝑏‘𝑧) ∈ (𝑐‘𝑧)) → ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜)) |
30 | | elpri 4145 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑧) ∈ {∅, 1𝑜}
→ ((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1𝑜)) |
31 | 30, 14 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑧) ∈ 2𝑜 → ((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1𝑜)) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) →
((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1𝑜)) |
33 | | orel2 397 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑏‘𝑧) = 1𝑜 → (((𝑏‘𝑧) = ∅ ∨ (𝑏‘𝑧) = 1𝑜) → (𝑏‘𝑧) = ∅)) |
34 | 32, 33 | mpan9 485 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ ¬
(𝑏‘𝑧) = 1𝑜) → (𝑏‘𝑧) = ∅) |
35 | 34 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜)) → (𝑏‘𝑧) = ∅) |
36 | | 0lt1o 7471 |
. . . . . . . . . . . 12
⊢ ∅
∈ 1𝑜 |
37 | 35, 36 | syl6eqel 2696 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜)) → (𝑏‘𝑧) ∈
1𝑜) |
38 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜)) → (𝑐‘𝑧) = 1𝑜) |
39 | 37, 38 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) ∧ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜)) → (𝑏‘𝑧) ∈ (𝑐‘𝑧)) |
40 | 29, 39 | impbida 873 |
. . . . . . . . 9
⊢ (((𝑏‘𝑧) ∈ 2𝑜 ∧ (𝑐‘𝑧) ∈ 2𝑜) →
((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜))) |
41 | 7, 10, 40 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜))) |
42 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → 𝑐 ∈ (2𝑜
↑𝑚 𝐴)) |
43 | 1 | pw2f1o2val2 36625 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑧) = 1𝑜)) |
44 | 42, 43 | sylancom 698 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑧) = 1𝑜)) |
45 | | simplrl 796 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → 𝑏 ∈ (2𝑜
↑𝑚 𝐴)) |
46 | 1 | pw2f1o2val2 36625 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑧) = 1𝑜)) |
47 | 45, 46 | sylancom 698 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (𝑧 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑧) = 1𝑜)) |
48 | 47 | notbid 307 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (¬ 𝑧 ∈ (𝐹‘𝑏) ↔ ¬ (𝑏‘𝑧) = 1𝑜)) |
49 | 44, 48 | anbi12d 743 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ↔ ((𝑐‘𝑧) = 1𝑜 ∧ ¬ (𝑏‘𝑧) = 1𝑜))) |
50 | 41, 49 | bitr4d 270 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) ∈ (𝑐‘𝑧) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
51 | 4, 50 | syl5bb 271 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → ((𝑏‘𝑧) E (𝑐‘𝑧) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
52 | 6 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → (𝑏‘𝑤) ∈
2𝑜) |
53 | 9 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → (𝑐‘𝑤) ∈
2𝑜) |
54 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ ((𝑏‘𝑤) = (𝑐‘𝑤) → ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) |
55 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → (𝑏‘𝑤) = ∅) |
56 | | 1n0 7462 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1𝑜 ≠ ∅ |
57 | 56 | nesymi 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
∅ = 1𝑜 |
58 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏‘𝑤) = ∅ → ((𝑏‘𝑤) = 1𝑜 ↔ ∅ =
1𝑜)) |
59 | 57, 58 | mtbiri 316 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏‘𝑤) = ∅ → ¬ (𝑏‘𝑤) = 1𝑜) |
60 | 59 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → ¬
(𝑏‘𝑤) = 1𝑜) |
61 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) |
62 | 60, 61 | mtbid 313 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → ¬
(𝑐‘𝑤) = 1𝑜) |
63 | | elpri 4145 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐‘𝑤) ∈ {∅, 1𝑜}
→ ((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1𝑜)) |
64 | 63, 14 | eleq2s 2706 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐‘𝑤) ∈ 2𝑜 → ((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1𝑜)) |
65 | 64 | ad3antlr 763 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → ((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1𝑜)) |
66 | | orel2 397 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑐‘𝑤) = 1𝑜 → (((𝑐‘𝑤) = ∅ ∨ (𝑐‘𝑤) = 1𝑜) → (𝑐‘𝑤) = ∅)) |
67 | 62, 65, 66 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → (𝑐‘𝑤) = ∅) |
68 | 55, 67 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = ∅) ∧ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) → (𝑏‘𝑤) = (𝑐‘𝑤)) |
69 | 68 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑤) ∈ 2𝑜 ∧ (𝑐‘𝑤) ∈ 2𝑜) ∧ (𝑏‘𝑤) = ∅) → (((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
70 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = 1𝑜) ∧
((𝑏‘𝑤) = 1𝑜 ↔
(𝑐‘𝑤) = 1𝑜)) → (𝑏‘𝑤) = 1𝑜) |
71 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = 1𝑜) ∧
((𝑏‘𝑤) = 1𝑜 ↔
(𝑐‘𝑤) = 1𝑜)) → ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜)) |
72 | 70, 71 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = 1𝑜) ∧
((𝑏‘𝑤) = 1𝑜 ↔
(𝑐‘𝑤) = 1𝑜)) → (𝑐‘𝑤) = 1𝑜) |
73 | 70, 72 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢
(((((𝑏‘𝑤) ∈ 2𝑜
∧ (𝑐‘𝑤) ∈ 2𝑜)
∧ (𝑏‘𝑤) = 1𝑜) ∧
((𝑏‘𝑤) = 1𝑜 ↔
(𝑐‘𝑤) = 1𝑜)) → (𝑏‘𝑤) = (𝑐‘𝑤)) |
74 | 73 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((((𝑏‘𝑤) ∈ 2𝑜 ∧ (𝑐‘𝑤) ∈ 2𝑜) ∧ (𝑏‘𝑤) = 1𝑜) → (((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
75 | | elpri 4145 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑤) ∈ {∅, 1𝑜}
→ ((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1𝑜)) |
76 | 75, 14 | eleq2s 2706 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑤) ∈ 2𝑜 → ((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1𝑜)) |
77 | 76 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑏‘𝑤) ∈ 2𝑜 ∧ (𝑐‘𝑤) ∈ 2𝑜) →
((𝑏‘𝑤) = ∅ ∨ (𝑏‘𝑤) = 1𝑜)) |
78 | 69, 74, 77 | mpjaodan 823 |
. . . . . . . . . . . 12
⊢ (((𝑏‘𝑤) ∈ 2𝑜 ∧ (𝑐‘𝑤) ∈ 2𝑜) →
(((𝑏‘𝑤) = 1𝑜 ↔
(𝑐‘𝑤) = 1𝑜) → (𝑏‘𝑤) = (𝑐‘𝑤))) |
79 | 54, 78 | impbid2 215 |
. . . . . . . . . . 11
⊢ (((𝑏‘𝑤) ∈ 2𝑜 ∧ (𝑐‘𝑤) ∈ 2𝑜) →
((𝑏‘𝑤) = (𝑐‘𝑤) ↔ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜))) |
80 | 52, 53, 79 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → ((𝑏‘𝑤) = (𝑐‘𝑤) ↔ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜))) |
81 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → 𝑏 ∈ (2𝑜
↑𝑚 𝐴)) |
82 | 1 | pw2f1o2val2 36625 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑤) = 1𝑜)) |
83 | 81, 82 | sylancom 698 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑏) ↔ (𝑏‘𝑤) = 1𝑜)) |
84 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → 𝑐 ∈ (2𝑜
↑𝑚 𝐴)) |
85 | 1 | pw2f1o2val2 36625 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑤) = 1𝑜)) |
86 | 84, 85 | sylancom 698 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → (𝑤 ∈ (𝐹‘𝑐) ↔ (𝑐‘𝑤) = 1𝑜)) |
87 | 83, 86 | bibi12d 334 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → ((𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)) ↔ ((𝑏‘𝑤) = 1𝑜 ↔ (𝑐‘𝑤) = 1𝑜))) |
88 | 80, 87 | bitr4d 270 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → ((𝑏‘𝑤) = (𝑐‘𝑤) ↔ (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))) |
89 | 88 | imbi2d 329 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑤 ∈ 𝐴) → ((𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
90 | 89 | ralbidva 2968 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
91 | 90 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
92 | 51, 91 | anbi12d 743 |
. . . . 5
⊢ (((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) ∧ 𝑧 ∈ 𝐴) → (((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))) ↔ ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
93 | 92 | rexbidva 3031 |
. . . 4
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) → (∃𝑧 ∈ 𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
94 | | vex 3176 |
. . . . 5
⊢ 𝑏 ∈ V |
95 | | vex 3176 |
. . . . 5
⊢ 𝑐 ∈ V |
96 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥‘𝑧) = (𝑏‘𝑧)) |
97 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑦 = 𝑐 → (𝑦‘𝑧) = (𝑐‘𝑧)) |
98 | 96, 97 | breqan12d 4599 |
. . . . . . 7
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑥‘𝑧) E (𝑦‘𝑧) ↔ (𝑏‘𝑧) E (𝑐‘𝑧))) |
99 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → (𝑥‘𝑤) = (𝑏‘𝑤)) |
100 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑐 → (𝑦‘𝑤) = (𝑐‘𝑤)) |
101 | 99, 100 | eqeqan12d 2626 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑏‘𝑤) = (𝑐‘𝑤))) |
102 | 101 | imbi2d 329 |
. . . . . . . 8
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → ((𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
103 | 102 | ralbidv 2969 |
. . . . . . 7
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
104 | 98, 103 | anbi12d 743 |
. . . . . 6
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))))) |
105 | 104 | rexbidv 3034 |
. . . . 5
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝑐) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤))))) |
106 | | wepwso.u |
. . . . 5
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧) E (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
107 | 94, 95, 105, 106 | braba 4917 |
. . . 4
⊢ (𝑏𝑈𝑐 ↔ ∃𝑧 ∈ 𝐴 ((𝑏‘𝑧) E (𝑐‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑏‘𝑤) = (𝑐‘𝑤)))) |
108 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘𝑏) ∈ V |
109 | | fvex 6113 |
. . . . 5
⊢ (𝐹‘𝑐) ∈ V |
110 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑐) → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ (𝐹‘𝑐))) |
111 | | eleq2 2677 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑏) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝐹‘𝑏))) |
112 | 111 | notbid 307 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑏) → (¬ 𝑧 ∈ 𝑥 ↔ ¬ 𝑧 ∈ (𝐹‘𝑏))) |
113 | 110, 112 | bi2anan9r 914 |
. . . . . . 7
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ↔ (𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)))) |
114 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐹‘𝑏) → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ (𝐹‘𝑏))) |
115 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑐) → (𝑤 ∈ 𝑦 ↔ 𝑤 ∈ (𝐹‘𝑐))) |
116 | 114, 115 | bi2bian9 915 |
. . . . . . . . 9
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦) ↔ (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))) |
117 | 116 | imbi2d 329 |
. . . . . . . 8
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → ((𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) ↔ (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
118 | 117 | ralbidv 2969 |
. . . . . . 7
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
119 | 113, 118 | anbi12d 743 |
. . . . . 6
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦))) ↔ ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
120 | 119 | rexbidv 3034 |
. . . . 5
⊢ ((𝑥 = (𝐹‘𝑏) ∧ 𝑦 = (𝐹‘𝑐)) → (∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦))) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐)))))) |
121 | | wepwso.t |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ 𝑦 ∧ ¬ 𝑧 ∈ 𝑥) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦)))} |
122 | 108, 109,
120, 121 | braba 4917 |
. . . 4
⊢ ((𝐹‘𝑏)𝑇(𝐹‘𝑐) ↔ ∃𝑧 ∈ 𝐴 ((𝑧 ∈ (𝐹‘𝑐) ∧ ¬ 𝑧 ∈ (𝐹‘𝑏)) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑤 ∈ (𝐹‘𝑏) ↔ 𝑤 ∈ (𝐹‘𝑐))))) |
123 | 93, 107, 122 | 3bitr4g 302 |
. . 3
⊢ ((𝐴 ∈ V ∧ (𝑏 ∈ (2𝑜
↑𝑚 𝐴) ∧ 𝑐 ∈ (2𝑜
↑𝑚 𝐴))) → (𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐))) |
124 | 123 | ralrimivva 2954 |
. 2
⊢ (𝐴 ∈ V → ∀𝑏 ∈ (2𝑜
↑𝑚 𝐴)∀𝑐 ∈ (2𝑜
↑𝑚 𝐴)(𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐))) |
125 | | df-isom 5813 |
. 2
⊢ (𝐹 Isom 𝑈, 𝑇 ((2𝑜
↑𝑚 𝐴), 𝒫 𝐴) ↔ (𝐹:(2𝑜
↑𝑚 𝐴)–1-1-onto→𝒫 𝐴 ∧ ∀𝑏 ∈ (2𝑜
↑𝑚 𝐴)∀𝑐 ∈ (2𝑜
↑𝑚 𝐴)(𝑏𝑈𝑐 ↔ (𝐹‘𝑏)𝑇(𝐹‘𝑐)))) |
126 | 2, 124, 125 | sylanbrc 695 |
1
⊢ (𝐴 ∈ V → 𝐹 Isom 𝑈, 𝑇 ((2𝑜
↑𝑚 𝐴), 𝒫 𝐴)) |