Proof of Theorem canth4
Step | Hyp | Ref
| Expression |
1 | | eqid 2824 |
. . . . . . . 8
⊢ 𝐵 = 𝐵 |
2 | | eqid 2824 |
. . . . . . . 8
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
3 | 1, 2 | pm3.2i 473 |
. . . . . . 7
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
4 | | canth4.1 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
5 | | elex 3515 |
. . . . . . . . 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 3970 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝑥 ∈ 𝐷) |
10 | 7, 9 | ffvelrnd 6855 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
11 | | canth4.2 |
. . . . . . . 8
⊢ 𝐵 = ∪
dom 𝑊 |
12 | 4, 6, 10, 11 | fpwwe 10071 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
13 | 3, 12 | mpbiri 260 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵)) |
14 | 13 | simpld 497 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵𝑊(𝑊‘𝐵)) |
15 | 4, 6 | fpwwelem 10070 |
. . . . 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 5952 |
. . . . 5
⊢ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⊆ dom (𝑊‘𝐵) |
21 | 19, 20 | eqsstri 4004 |
. . . 4
⊢ 𝐶 ⊆ dom (𝑊‘𝐵) |
22 | 17 | simprd 498 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) |
23 | | dmss 5774 |
. . . . . 6
⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
25 | | dmxpid 5803 |
. . . . 5
⊢ dom
(𝐵 × 𝐵) = 𝐵 |
26 | 24, 25 | sseqtrdi 4020 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ 𝐵) |
27 | 21, 26 | sstrid 3981 |
. . 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 5549 |
. . . . . 6
⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) Or 𝐵) |
33 | | sonr 5499 |
. . . . 5
⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐹‘𝐵) ∈ 𝐵) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
34 | 32, 28, 33 | syl2anc 586 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
35 | 19 | eleq2i 2907 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
36 | | fvex 6686 |
. . . . . 6
⊢ (𝐹‘𝐵) ∈ V |
37 | 36 | eliniseg 5961 |
. . . . . 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 4092 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊊ 𝐵) |
42 | | sneq 4580 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝐵) → {𝑦} = {(𝐹‘𝐵)}) |
43 | 42 | imaeq2d 5932 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
44 | 43, 19 | syl6eqr 2877 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = 𝐶) |
45 | 44 | fveq2d 6677 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = (𝐹‘𝐶)) |
46 | | id 22 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → 𝑦 = (𝐹‘𝐵)) |
47 | 45, 46 | eqeq12d 2840 |
. . . 4
⊢ (𝑦 = (𝐹‘𝐵) → ((𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦 ↔ (𝐹‘𝐶) = (𝐹‘𝐵))) |
48 | 29 | simprd 498 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦) |
49 | 47, 48, 28 | rspcdva 3628 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐶) = (𝐹‘𝐵)) |
50 | 49 | eqcomd 2830 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) = (𝐹‘𝐶)) |
51 | 18, 41, 50 | 3jca 1124 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |