Proof of Theorem canthnumlem
Step | Hyp | Ref
| Expression |
1 | | f1f 6443 |
. . . . 5
⊢ (𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴 → 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) |
2 | | ssid 3910 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
dom card) ⊆ (𝒫 𝐴 ∩ dom card) |
3 | | canth4.1 |
. . . . . . 7
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
4 | | canth4.2 |
. . . . . . 7
⊢ 𝐵 = ∪
dom 𝑊 |
5 | | canth4.3 |
. . . . . . 7
⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) |
6 | 3, 4, 5 | canth4 9915 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ (𝒫 𝐴 ∩ dom card)) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
7 | 2, 6 | mp3an3 1442 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
8 | 1, 7 | sylan2 592 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
9 | 8 | simp3d 1137 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐹‘𝐵) = (𝐹‘𝐶)) |
10 | | simpr 485 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |
11 | 8 | simp1d 1135 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ⊆ 𝐴) |
12 | | elpw2g 5138 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
14 | 11, 13 | mpbird 258 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ 𝒫 𝐴) |
15 | | eqid 2795 |
. . . . . . . . . . . 12
⊢ 𝐵 = 𝐵 |
16 | | eqid 2795 |
. . . . . . . . . . . 12
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
17 | 15, 16 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
18 | | elex 3455 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐴 ∈ V) |
20 | 10, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) |
21 | 20 | ffvelrnda 6716 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
22 | 3, 19, 21, 4 | fpwwe 9914 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
23 | 17, 22 | mpbiri 259 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵)) |
24 | 23 | simpld 495 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵𝑊(𝑊‘𝐵)) |
25 | 3, 19 | fpwwelem 9913 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) |
26 | 24, 25 | mpbid 233 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) |
27 | 26 | simprld 768 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝑊‘𝐵) We 𝐵) |
28 | | fvex 6551 |
. . . . . . . 8
⊢ (𝑊‘𝐵) ∈ V |
29 | | weeq1 5431 |
. . . . . . . 8
⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵)) |
30 | 28, 29 | spcev 3549 |
. . . . . . 7
⊢ ((𝑊‘𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵) |
31 | 27, 30 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ∃𝑟 𝑟 We 𝐵) |
32 | | ween 9307 |
. . . . . 6
⊢ (𝐵 ∈ dom card ↔
∃𝑟 𝑟 We 𝐵) |
33 | 31, 32 | sylibr 235 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ dom card) |
34 | 14, 33 | elind 4092 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ (𝒫 𝐴 ∩ dom card)) |
35 | 8 | simp2d 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊊ 𝐵) |
36 | 35 | pssssd 3995 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊆ 𝐵) |
37 | 36, 11 | sstrd 3899 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊆ 𝐴) |
38 | | elpw2g 5138 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
40 | 37, 39 | mpbird 258 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ 𝒫 𝐴) |
41 | | ssnum 9311 |
. . . . . 6
⊢ ((𝐵 ∈ dom card ∧ 𝐶 ⊆ 𝐵) → 𝐶 ∈ dom card) |
42 | 33, 36, 41 | syl2anc 584 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ dom card) |
43 | 40, 42 | elind 4092 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ (𝒫 𝐴 ∩ dom card)) |
44 | | f1fveq 6885 |
. . . 4
⊢ ((𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∩ dom card) ∧ 𝐶 ∈ (𝒫 𝐴 ∩ dom card))) → ((𝐹‘𝐵) = (𝐹‘𝐶) ↔ 𝐵 = 𝐶)) |
45 | 10, 34, 43, 44 | syl12anc 833 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐶) ↔ 𝐵 = 𝐶)) |
46 | 9, 45 | mpbid 233 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 = 𝐶) |
47 | 35 | pssned 3996 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ≠ 𝐵) |
48 | 47 | necomd 3039 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ≠ 𝐶) |
49 | 48 | neneqd 2989 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ¬ 𝐵 = 𝐶) |
50 | 46, 49 | pm2.65da 813 |
1
⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |