Proof of Theorem canth4
Step | Hyp | Ref
| Expression |
1 | | eqid 2823 |
. . . . . . . 8
⊢ 𝐵 = 𝐵 |
2 | | eqid 2823 |
. . . . . . . 8
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
3 | 1, 2 | pm3.2i 473 |
. . . . . . 7
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
4 | | canth4.1 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
5 | | elex 3514 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
6 | 5 | 3ad2ant1 1129 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐴 ∈ V) |
7 | | simpl2 1188 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝐹:𝐷⟶𝐴) |
8 | | simp3 1134 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) |
9 | 8 | sselda 3969 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝑥 ∈ 𝐷) |
10 | 7, 9 | ffvelrnd 6854 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
11 | | canth4.2 |
. . . . . . . 8
⊢ 𝐵 = ∪
dom 𝑊 |
12 | 4, 6, 10, 11 | fpwwe 10070 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
13 | 3, 12 | mpbiri 260 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵)) |
14 | 13 | simpld 497 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵𝑊(𝑊‘𝐵)) |
15 | 4, 6 | fpwwelem 10069 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) |
16 | 14, 15 | mpbid 234 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) |
17 | 16 | simpld 497 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))) |
18 | 17 | simpld 497 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵 ⊆ 𝐴) |
19 | | canth4.3 |
. . . . 5
⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) |
20 | | cnvimass 5951 |
. . . . 5
⊢ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⊆ dom (𝑊‘𝐵) |
21 | 19, 20 | eqsstri 4003 |
. . . 4
⊢ 𝐶 ⊆ dom (𝑊‘𝐵) |
22 | 17 | simprd 498 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) |
23 | | dmss 5773 |
. . . . . 6
⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
25 | | dmxpid 5802 |
. . . . 5
⊢ dom
(𝐵 × 𝐵) = 𝐵 |
26 | 24, 25 | sseqtrdi 4019 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ 𝐵) |
27 | 21, 26 | sstrid 3980 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊆ 𝐵) |
28 | 13 | simprd 498 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) ∈ 𝐵) |
29 | 16 | simprd 498 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)) |
30 | 29 | simpld 497 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) We 𝐵) |
31 | | weso 5548 |
. . . . . 6
⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) Or 𝐵) |
33 | | sonr 5498 |
. . . . 5
⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐹‘𝐵) ∈ 𝐵) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
34 | 32, 28, 33 | syl2anc 586 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
35 | 19 | eleq2i 2906 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
36 | | fvex 6685 |
. . . . . 6
⊢ (𝐹‘𝐵) ∈ V |
37 | 36 | eliniseg 5960 |
. . . . . 6
⊢ ((𝐹‘𝐵) ∈ V → ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
39 | 35, 38 | bitri 277 |
. . . 4
⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
40 | 34, 39 | sylnibr 331 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵) ∈ 𝐶) |
41 | 27, 28, 40 | ssnelpssd 4091 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊊ 𝐵) |
42 | | sneq 4579 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝐵) → {𝑦} = {(𝐹‘𝐵)}) |
43 | 42 | imaeq2d 5931 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
44 | 43, 19 | syl6eqr 2876 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = 𝐶) |
45 | 44 | fveq2d 6676 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = (𝐹‘𝐶)) |
46 | | id 22 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → 𝑦 = (𝐹‘𝐵)) |
47 | 45, 46 | eqeq12d 2839 |
. . . 4
⊢ (𝑦 = (𝐹‘𝐵) → ((𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦 ↔ (𝐹‘𝐶) = (𝐹‘𝐵))) |
48 | 29 | simprd 498 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦) |
49 | 47, 48, 28 | rspcdva 3627 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐶) = (𝐹‘𝐵)) |
50 | 49 | eqcomd 2829 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) = (𝐹‘𝐶)) |
51 | 18, 41, 50 | 3jca 1124 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |