Proof of Theorem canthnumlem
Step | Hyp | Ref
| Expression |
1 | | f1f 6615 |
. . . . 5
⊢ (𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴 → 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) |
2 | | ssid 3923 |
. . . . . 6
⊢
(𝒫 𝐴 ∩
dom card) ⊆ (𝒫 𝐴 ∩ dom card) |
3 | | canth4.1 |
. . . . . . 7
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
4 | | canth4.2 |
. . . . . . 7
⊢ 𝐵 = ∪
dom 𝑊 |
5 | | canth4.3 |
. . . . . . 7
⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) |
6 | 3, 4, 5 | canth4 10261 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ (𝒫 𝐴 ∩ dom card)) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
7 | 2, 6 | mp3an3 1452 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
8 | 1, 7 | sylan2 596 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |
9 | 8 | simp3d 1146 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐹‘𝐵) = (𝐹‘𝐶)) |
10 | | simpr 488 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |
11 | 8 | simp1d 1144 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ⊆ 𝐴) |
12 | | elpw2g 5237 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
13 | 12 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
14 | 11, 13 | mpbird 260 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ 𝒫 𝐴) |
15 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ 𝐵 = 𝐵 |
16 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
17 | 15, 16 | pm3.2i 474 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
18 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐴 ∈ 𝑉) |
19 | 10, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐹:(𝒫 𝐴 ∩ dom card)⟶𝐴) |
20 | 19 | ffvelrnda 6904 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
21 | 3, 18, 20, 4 | fpwwe 10260 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
22 | 17, 21 | mpbiri 261 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵)) |
23 | 22 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵𝑊(𝑊‘𝐵)) |
24 | 3, 18 | fpwwelem 10259 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) |
25 | 23, 24 | mpbid 235 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) |
26 | 25 | simprld 772 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝑊‘𝐵) We 𝐵) |
27 | | fvex 6730 |
. . . . . . . 8
⊢ (𝑊‘𝐵) ∈ V |
28 | | weeq1 5539 |
. . . . . . . 8
⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵)) |
29 | 27, 28 | spcev 3521 |
. . . . . . 7
⊢ ((𝑊‘𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵) |
30 | 26, 29 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ∃𝑟 𝑟 We 𝐵) |
31 | | ween 9649 |
. . . . . 6
⊢ (𝐵 ∈ dom card ↔
∃𝑟 𝑟 We 𝐵) |
32 | 30, 31 | sylibr 237 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ dom card) |
33 | 14, 32 | elind 4108 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ∈ (𝒫 𝐴 ∩ dom card)) |
34 | 8 | simp2d 1145 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊊ 𝐵) |
35 | 34 | pssssd 4012 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊆ 𝐵) |
36 | 35, 11 | sstrd 3911 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ⊆ 𝐴) |
37 | | elpw2g 5237 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
38 | 37 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → (𝐶 ∈ 𝒫 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
39 | 36, 38 | mpbird 260 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ 𝒫 𝐴) |
40 | | ssnum 9653 |
. . . . . 6
⊢ ((𝐵 ∈ dom card ∧ 𝐶 ⊆ 𝐵) → 𝐶 ∈ dom card) |
41 | 32, 35, 40 | syl2anc 587 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ dom card) |
42 | 39, 41 | elind 4108 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ∈ (𝒫 𝐴 ∩ dom card)) |
43 | | f1fveq 7074 |
. . . 4
⊢ ((𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∩ dom card) ∧ 𝐶 ∈ (𝒫 𝐴 ∩ dom card))) → ((𝐹‘𝐵) = (𝐹‘𝐶) ↔ 𝐵 = 𝐶)) |
44 | 10, 33, 42, 43 | syl12anc 837 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ((𝐹‘𝐵) = (𝐹‘𝐶) ↔ 𝐵 = 𝐶)) |
45 | 9, 44 | mpbid 235 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 = 𝐶) |
46 | 34 | pssned 4013 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐶 ≠ 𝐵) |
47 | 46 | necomd 2996 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → 𝐵 ≠ 𝐶) |
48 | 47 | neneqd 2945 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) → ¬ 𝐵 = 𝐶) |
49 | 45, 48 | pm2.65da 817 |
1
⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) |