Proof of Theorem canthp1lem2
Step | Hyp | Ref
| Expression |
1 | | canthp1lem2.1 |
. . . . . 6
⊢ (𝜑 → 1o ≺
𝐴) |
2 | | relsdom 8307 |
. . . . . . 7
⊢ Rel
≺ |
3 | 2 | brrelex2i 5453 |
. . . . . 6
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) |
4 | 1, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
5 | 4 | pwexd 5127 |
. . . 4
⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
6 | | canthp1lem2.2 |
. . . 4
⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o)) |
7 | | f1oeng 8319 |
. . . 4
⊢
((𝒫 𝐴 ∈
V ∧ 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o)) → 𝒫
𝐴 ≈ (𝐴 ⊔
1o)) |
8 | 5, 6, 7 | syl2anc 576 |
. . 3
⊢ (𝜑 → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o)) |
9 | 8 | ensymd 8351 |
. 2
⊢ (𝜑 → (𝐴 ⊔ 1o) ≈ 𝒫
𝐴) |
10 | | canth2g 8461 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) |
11 | 4, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≺ 𝒫 𝐴) |
12 | | sdomen2 8452 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ≈
(𝐴 ⊔ 1o)
→ (𝐴 ≺ 𝒫
𝐴 ↔ 𝐴 ≺ (𝐴 ⊔ 1o))) |
13 | 8, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ≺ 𝒫 𝐴 ↔ 𝐴 ≺ (𝐴 ⊔ 1o))) |
14 | 11, 13 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≺ (𝐴 ⊔ 1o)) |
15 | | sdomnen 8329 |
. . . . . . . . 9
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → ¬ 𝐴 ≈ (𝐴 ⊔ 1o)) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝐴 ≈ (𝐴 ⊔ 1o)) |
17 | | omelon 8897 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
18 | | onenon 9166 |
. . . . . . . . . . . 12
⊢ (ω
∈ On → ω ∈ dom card) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ω
∈ dom card |
20 | | canthp1lem2.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴) |
21 | | dff1o3 6444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) ↔ (𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o) ∧ Fun ◡𝐹)) |
22 | 21 | simprbi 489 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → Fun ◡𝐹) |
23 | 6, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun ◡𝐹) |
24 | | f1ofo 6445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o)) |
25 | 6, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o)) |
26 | | f1ofn 6439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → 𝐹 Fn 𝒫 𝐴) |
27 | | fnresdm 6293 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹) |
28 | | foeq1 6409 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o))) |
29 | 6, 26, 27, 28 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o))) |
30 | 25, 29 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o)) |
31 | | fvex 6506 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹‘𝐴) ∈ V |
32 | | f1osng 6478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ V ∧ (𝐹‘𝐴) ∈ V) → {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)}) |
33 | 4, 31, 32 | sylancl 577 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)}) |
34 | 6, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) |
35 | | pwidg 4431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) |
36 | 4, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐴) |
37 | | fnressn 6737 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ 𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {〈𝐴, (𝐹‘𝐴)〉}) |
38 | 34, 36, 37 | syl2anc 576 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐹 ↾ {𝐴}) = {〈𝐴, (𝐹‘𝐴)〉}) |
39 | | f1oeq1 6427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 ↾ {𝐴}) = {〈𝐴, (𝐹‘𝐴)〉} → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)} ↔ {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)})) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)} ↔ {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)})) |
41 | 33, 40 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)}) |
42 | | f1ofo 6445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) |
44 | | resdif 6458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
◡𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) |
45 | 23, 30, 43, 44 | syl3anc 1351 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) |
46 | | f1oco 6460 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) |
47 | 20, 45, 46 | syl2anc 576 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) |
48 | | resco 5936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) |
49 | | f1oeq1 6427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴)) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) |
51 | 47, 50 | sylibr 226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) |
52 | | f1of 6438 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴) |
54 | | 0elpw 5104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
∈ 𝒫 𝐴 |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴) |
56 | | sdom0 8439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ¬
1o ≺ ∅ |
57 | | breq2 4927 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∅
= 𝐴 → (1o
≺ ∅ ↔ 1o ≺ 𝐴)) |
58 | 56, 57 | mtbii 318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
= 𝐴 → ¬
1o ≺ 𝐴) |
59 | 58 | necon2ai 2990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1o ≺ 𝐴 → ∅ ≠ 𝐴) |
60 | 1, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∅ ≠ 𝐴) |
61 | 60 | ad2antrr 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴) |
62 | | eldifsn 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ (𝒫 𝐴 ∖
{𝐴}) ↔ (∅ ∈
𝒫 𝐴 ∧ ∅
≠ 𝐴)) |
63 | 55, 61, 62 | sylanbrc 575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴})) |
64 | | simplr 756 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴) |
65 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴) |
66 | 65 | neqned 2968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ≠ 𝐴) |
67 | | eldifsn 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ≠ 𝐴)) |
68 | 64, 66, 67 | sylanbrc 575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴})) |
69 | 63, 68 | ifclda 4378 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴})) |
70 | 69 | fmpttd 6696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) |
71 | | fco 6355 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴⟶𝐴) |
72 | 53, 70, 71 | syl2anc 576 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴⟶𝐴) |
73 | 70 | frnd 6345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴})) |
74 | | cores 5935 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))) |
76 | | canthp1lem2.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) |
77 | 75, 76 | syl6eqr 2826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻) |
78 | 77 | feq1d 6323 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴⟶𝐴 ↔ 𝐻:𝒫 𝐴⟶𝐴)) |
79 | 72, 78 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:𝒫 𝐴⟶𝐴) |
80 | | inss1 4086 |
. . . . . . . . . . . . . . . 16
⊢
(𝒫 𝐴 ∩
dom card) ⊆ 𝒫 𝐴 |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆
𝒫 𝐴) |
82 | | canthp1lem2.5 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))} |
83 | | canthp1lem2.6 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 = ∪
dom 𝑊 |
84 | | eqid 2772 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) |
85 | 82, 83, 84 | canth4 9861 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵 ⊆ 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵 ∧ (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
86 | 4, 79, 81, 85 | syl3anc 1351 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ⊆ 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵 ∧ (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
87 | 86 | simp1d 1122 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
88 | 86 | simp2d 1123 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵) |
89 | 88 | pssned 3959 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐵) |
90 | 89 | necomd 3016 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
91 | 86 | simp3d 1124 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
92 | 76 | fveq1i 6494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻‘𝐵) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) |
93 | 76 | fveq1i 6494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
94 | 91, 92, 93 | 3eqtr3g 2831 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
95 | 4, 87 | sselpwd 5080 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴) |
96 | | fvco3 6582 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ 𝐵 ∈ 𝒫 𝐴) → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵))) |
97 | 70, 95, 96 | syl2anc 576 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵))) |
98 | 88 | pssssd 3958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐵) |
99 | 98, 87 | sstrd 3862 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐴) |
100 | 4, 99 | sselpwd 5080 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) |
101 | | fvco3 6582 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
102 | 70, 100, 101 | syl2anc 576 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
103 | 94, 97, 102 | 3eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
104 | 103 | adantr 473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) |
105 | | eqid 2772 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) |
106 | | eqeq1 2776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝐵 → (𝑥 = 𝐴 ↔ 𝐵 = 𝐴)) |
107 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
108 | 106, 107 | ifbieq2d 4369 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵)) |
109 | | ifcl 4388 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) |
110 | 54, 95, 109 | sylancr 578 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) |
111 | 105, 108,
95, 110 | fvmptd3 6611 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵)) |
112 | | pssne 3957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ⊊ 𝐴 → 𝐵 ≠ 𝐴) |
113 | 112 | neneqd 2966 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐵 = 𝐴) |
114 | 113 | iffalsed 4355 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ⊊ 𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵) |
115 | 111, 114 | sylan9eq 2828 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵) |
116 | 115 | fveq2d 6497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘𝐵)) |
117 | | eqeq1 2776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → (𝑥 = 𝐴 ↔ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴)) |
118 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → 𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
119 | 117, 118 | ifbieq2d 4369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
120 | | ifcl 4388 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((∅
∈ 𝒫 𝐴 ∧
(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ∈ 𝒫 𝐴) |
121 | 54, 100, 120 | sylancr 578 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ∈ 𝒫 𝐴) |
122 | 105, 119,
100, 121 | fvmptd3 6611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
123 | 122 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
124 | | sspsstr 3966 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐴) |
125 | 98, 124 | sylan 572 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐴) |
126 | 125 | pssned 3959 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐴) |
127 | 126 | neneqd 2966 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ¬ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴) |
128 | 127 | iffalsed 4355 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
129 | 123, 128 | eqtrd 2808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
130 | 129 | fveq2d 6497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
131 | 104, 116,
130 | 3eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘𝐵) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
132 | 95, 112 | anim12i 603 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴)) |
133 | | eldifsn 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴)) |
134 | 132, 133 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴})) |
135 | 134 | fvresd 6513 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺 ∘ 𝐹)‘𝐵)) |
136 | 100 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) |
137 | | eldifsn 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ ((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐴)) |
138 | 136, 126,
137 | sylanbrc 575 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴})) |
139 | 138 | fvresd 6513 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
140 | 131, 135,
139 | 3eqtr4d 2818 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
141 | | f1of1 6437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) |
142 | 51, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) |
143 | 142 | adantr 473 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) |
144 | | f1fveq 6839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ↔ 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
145 | 143, 134,
138, 144 | syl12anc 824 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ↔ 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
146 | 140, 145 | mpbid 224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) |
147 | 146 | ex 405 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 ⊊ 𝐴 → 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) |
148 | 147 | necon3ad 2974 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 ≠ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → ¬ 𝐵 ⊊ 𝐴)) |
149 | 90, 148 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐵 ⊊ 𝐴) |
150 | | npss 3971 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐵 ⊊ 𝐴 ↔ (𝐵 ⊆ 𝐴 → 𝐵 = 𝐴)) |
151 | 149, 150 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 ⊆ 𝐴 → 𝐵 = 𝐴)) |
152 | 87, 151 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = 𝐴) |
153 | | eqid 2772 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = 𝐵 |
154 | | eqid 2772 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
155 | 153, 154 | pm3.2i 463 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
156 | | elinel1 4054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴) |
157 | | ffvelrn 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐻:𝒫 𝐴⟶𝐴 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝐻‘𝑥) ∈ 𝐴) |
158 | 79, 156, 157 | syl2an 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻‘𝑥) ∈ 𝐴) |
159 | 82, 4, 158, 83 | fpwwe 9860 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐻‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
160 | 155, 159 | mpbiri 250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐻‘𝐵) ∈ 𝐵)) |
161 | 160 | simpld 487 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵𝑊(𝑊‘𝐵)) |
162 | 82, 4 | fpwwelem 9859 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐻‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) |
163 | 161, 162 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐻‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) |
164 | 163 | simprld 759 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊‘𝐵) We 𝐵) |
165 | | fvex 6506 |
. . . . . . . . . . . . . . 15
⊢ (𝑊‘𝐵) ∈ V |
166 | | weeq1 5389 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵)) |
167 | 165, 166 | spcev 3519 |
. . . . . . . . . . . . . 14
⊢ ((𝑊‘𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵) |
168 | 164, 167 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑟 𝑟 We 𝐵) |
169 | | ween 9249 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card ↔
∃𝑟 𝑟 We 𝐵) |
170 | 168, 169 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ dom card) |
171 | 152, 170 | eqeltrrd 2861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ dom card) |
172 | | domtri2 9206 |
. . . . . . . . . . 11
⊢ ((ω
∈ dom card ∧ 𝐴
∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω)) |
173 | 19, 171, 172 | sylancr 578 |
. . . . . . . . . 10
⊢ (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω)) |
174 | | infdju1 9407 |
. . . . . . . . . 10
⊢ (ω
≼ 𝐴 → (𝐴 ⊔ 1o) ≈
𝐴) |
175 | 173, 174 | syl6bir 246 |
. . . . . . . . 9
⊢ (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 ⊔ 1o) ≈ 𝐴)) |
176 | | ensym 8349 |
. . . . . . . . 9
⊢ ((𝐴 ⊔ 1o) ≈
𝐴 → 𝐴 ≈ (𝐴 ⊔ 1o)) |
177 | 175, 176 | syl6 35 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 ⊔ 1o))) |
178 | 16, 177 | mt3d 143 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≺ ω) |
179 | | 2onn 8061 |
. . . . . . . 8
⊢
2o ∈ ω |
180 | | nnsdom 8905 |
. . . . . . . 8
⊢
(2o ∈ ω → 2o ≺
ω) |
181 | 179, 180 | ax-mp 5 |
. . . . . . 7
⊢
2o ≺ ω |
182 | | djufi 9404 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧
2o ≺ ω) → (𝐴 ⊔ 2o) ≺
ω) |
183 | 178, 181,
182 | sylancl 577 |
. . . . . 6
⊢ (𝜑 → (𝐴 ⊔ 2o) ≺
ω) |
184 | | isfinite 8903 |
. . . . . 6
⊢ ((𝐴 ⊔ 2o) ∈
Fin ↔ (𝐴 ⊔
2o) ≺ ω) |
185 | 183, 184 | sylibr 226 |
. . . . 5
⊢ (𝜑 → (𝐴 ⊔ 2o) ∈
Fin) |
186 | | sssucid 6100 |
. . . . . . . . . 10
⊢
1o ⊆ suc 1o |
187 | | df-2o 7900 |
. . . . . . . . . 10
⊢
2o = suc 1o |
188 | 186, 187 | sseqtr4i 3888 |
. . . . . . . . 9
⊢
1o ⊆ 2o |
189 | | xpss2 5421 |
. . . . . . . . 9
⊢
(1o ⊆ 2o → ({1o} ×
1o) ⊆ ({1o} ×
2o)) |
190 | 188, 189 | ax-mp 5 |
. . . . . . . 8
⊢
({1o} × 1o) ⊆ ({1o} ×
2o) |
191 | | unss2 4039 |
. . . . . . . 8
⊢
(({1o} × 1o) ⊆ ({1o}
× 2o) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o))) |
192 | 190, 191 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o))) |
193 | | ssun2 4032 |
. . . . . . . . 9
⊢
({1o} × 2o) ⊆ (({∅} ×
𝐴) ∪ ({1o}
× 2o)) |
194 | | 1oex 7907 |
. . . . . . . . . . 11
⊢
1o ∈ V |
195 | 194 | snid 4467 |
. . . . . . . . . 10
⊢
1o ∈ {1o} |
196 | 194 | sucid 6102 |
. . . . . . . . . . 11
⊢
1o ∈ suc 1o |
197 | 196, 187 | eleqtrri 2859 |
. . . . . . . . . 10
⊢
1o ∈ 2o |
198 | | opelxpi 5438 |
. . . . . . . . . 10
⊢
((1o ∈ {1o} ∧ 1o ∈
2o) → 〈1o, 1o〉 ∈
({1o} × 2o)) |
199 | 195, 197,
198 | mp2an 679 |
. . . . . . . . 9
⊢
〈1o, 1o〉 ∈ ({1o} ×
2o) |
200 | 193, 199 | sselii 3849 |
. . . . . . . 8
⊢
〈1o, 1o〉 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 2o)) |
201 | | 1n0 7915 |
. . . . . . . . . . . 12
⊢
1o ≠ ∅ |
202 | 201 | neii 2963 |
. . . . . . . . . . 11
⊢ ¬
1o = ∅ |
203 | | opelxp1 5442 |
. . . . . . . . . . . 12
⊢
(〈1o, 1o〉 ∈ ({∅} ×
𝐴) → 1o
∈ {∅}) |
204 | | elsni 4452 |
. . . . . . . . . . . 12
⊢
(1o ∈ {∅} → 1o =
∅) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . 11
⊢
(〈1o, 1o〉 ∈ ({∅} ×
𝐴) → 1o =
∅) |
206 | 202, 205 | mto 189 |
. . . . . . . . . 10
⊢ ¬
〈1o, 1o〉 ∈ ({∅} × 𝐴) |
207 | | 1onn 8060 |
. . . . . . . . . . . 12
⊢
1o ∈ ω |
208 | | nnord 7398 |
. . . . . . . . . . . 12
⊢
(1o ∈ ω → Ord 1o) |
209 | | ordirr 6041 |
. . . . . . . . . . . 12
⊢ (Ord
1o → ¬ 1o ∈ 1o) |
210 | 207, 208,
209 | mp2b 10 |
. . . . . . . . . . 11
⊢ ¬
1o ∈ 1o |
211 | | opelxp2 5443 |
. . . . . . . . . . 11
⊢
(〈1o, 1o〉 ∈ ({1o}
× 1o) → 1o ∈
1o) |
212 | 210, 211 | mto 189 |
. . . . . . . . . 10
⊢ ¬
〈1o, 1o〉 ∈ ({1o} ×
1o) |
213 | 206, 212 | pm3.2ni 864 |
. . . . . . . . 9
⊢ ¬
(〈1o, 1o〉 ∈ ({∅} × 𝐴) ∨ 〈1o,
1o〉 ∈ ({1o} ×
1o)) |
214 | | elun 4008 |
. . . . . . . . 9
⊢
(〈1o, 1o〉 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 1o)) ↔ (〈1o, 1o〉 ∈
({∅} × 𝐴) ∨
〈1o, 1o〉 ∈ ({1o} ×
1o))) |
215 | 213, 214 | mtbir 315 |
. . . . . . . 8
⊢ ¬
〈1o, 1o〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o)) |
216 | | ssnelpss 3972 |
. . . . . . . 8
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o)) → ((〈1o, 1o〉 ∈
(({∅} × 𝐴)
∪ ({1o} × 2o)) ∧ ¬ 〈1o,
1o〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o))) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o)))) |
217 | 200, 215,
216 | mp2ani 685 |
. . . . . . 7
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o)) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) |
218 | 192, 217 | syl 17 |
. . . . . 6
⊢ (𝜑 → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) |
219 | | df-dju 9118 |
. . . . . . 7
⊢ (𝐴 ⊔ 1o) =
(({∅} × 𝐴)
∪ ({1o} × 1o)) |
220 | | df-dju 9118 |
. . . . . . 7
⊢ (𝐴 ⊔ 2o) =
(({∅} × 𝐴)
∪ ({1o} × 2o)) |
221 | 219, 220 | psseq12i 3952 |
. . . . . 6
⊢ ((𝐴 ⊔ 1o)
⊊ (𝐴 ⊔
2o) ↔ (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) |
222 | 218, 221 | sylibr 226 |
. . . . 5
⊢ (𝜑 → (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔
2o)) |
223 | | php3 8493 |
. . . . 5
⊢ (((𝐴 ⊔ 2o) ∈
Fin ∧ (𝐴 ⊔
1o) ⊊ (𝐴
⊔ 2o)) → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔
2o)) |
224 | 185, 222,
223 | syl2anc 576 |
. . . 4
⊢ (𝜑 → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔
2o)) |
225 | | canthp1lem1 9866 |
. . . . 5
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |
226 | 1, 225 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) |
227 | | sdomdomtr 8440 |
. . . 4
⊢ (((𝐴 ⊔ 1o) ≺
(𝐴 ⊔ 2o)
∧ (𝐴 ⊔
2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 1o) ≺ 𝒫
𝐴) |
228 | 224, 226,
227 | syl2anc 576 |
. . 3
⊢ (𝜑 → (𝐴 ⊔ 1o) ≺ 𝒫
𝐴) |
229 | | sdomnen 8329 |
. . 3
⊢ ((𝐴 ⊔ 1o) ≺
𝒫 𝐴 → ¬
(𝐴 ⊔ 1o)
≈ 𝒫 𝐴) |
230 | 228, 229 | syl 17 |
. 2
⊢ (𝜑 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫
𝐴) |
231 | 9, 230 | pm2.65i 186 |
1
⊢ ¬
𝜑 |