Proof of Theorem canth4
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . 8
⊢ 𝐵 = 𝐵 |
2 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
3 | 1, 2 | pm3.2i 471 |
. . . . . . 7
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
4 | | canth4.1 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} |
5 | | elex 3212 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
6 | 5 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐴 ∈ V) |
7 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝐹:𝐷⟶𝐴) |
8 | | simp3 1063 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) |
9 | 8 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → 𝑥 ∈ 𝐷) |
10 | 7, 9 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) |
11 | | canth4.2 |
. . . . . . . 8
⊢ 𝐵 = ∪
dom 𝑊 |
12 | 4, 6, 10, 11 | fpwwe 9468 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
13 | 3, 12 | mpbiri 248 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐹‘𝐵) ∈ 𝐵)) |
14 | 13 | simpld 475 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵𝑊(𝑊‘𝐵)) |
15 | 4, 6 | fpwwelem 9467 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) |
16 | 14, 15 | mpbid 222 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) |
17 | 16 | simpld 475 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))) |
18 | 17 | simpld 475 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐵 ⊆ 𝐴) |
19 | | canth4.3 |
. . . . 5
⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) |
20 | | cnvimass 5485 |
. . . . 5
⊢ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⊆ dom (𝑊‘𝐵) |
21 | 19, 20 | eqsstri 3635 |
. . . 4
⊢ 𝐶 ⊆ dom (𝑊‘𝐵) |
22 | 17 | simprd 479 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) |
23 | | dmss 5323 |
. . . . . 6
⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
24 | 22, 23 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
25 | | dmxpid 5345 |
. . . . 5
⊢ dom
(𝐵 × 𝐵) = 𝐵 |
26 | 24, 25 | syl6sseq 3651 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → dom (𝑊‘𝐵) ⊆ 𝐵) |
27 | 21, 26 | syl5ss 3614 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊆ 𝐵) |
28 | 13 | simprd 479 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) ∈ 𝐵) |
29 | 16 | simprd 479 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)) |
30 | 29 | simpld 475 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) We 𝐵) |
31 | | weso 5105 |
. . . . . 6
⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝑊‘𝐵) Or 𝐵) |
33 | | sonr 5056 |
. . . . 5
⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐹‘𝐵) ∈ 𝐵) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
34 | 32, 28, 33 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
35 | 19 | eleq2i 2693 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
36 | | fvex 6201 |
. . . . . 6
⊢ (𝐹‘𝐵) ∈ V |
37 | 36 | eliniseg 5494 |
. . . . . 6
⊢ ((𝐹‘𝐵) ∈ V → ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵))) |
38 | 36, 37 | ax-mp 5 |
. . . . 5
⊢ ((𝐹‘𝐵) ∈ (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
39 | 35, 38 | bitri 264 |
. . . 4
⊢ ((𝐹‘𝐵) ∈ 𝐶 ↔ (𝐹‘𝐵)(𝑊‘𝐵)(𝐹‘𝐵)) |
40 | 34, 39 | sylnibr 319 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ¬ (𝐹‘𝐵) ∈ 𝐶) |
41 | 27, 28, 40 | ssnelpssd 3719 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → 𝐶 ⊊ 𝐵) |
42 | 29 | simprd 479 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → ∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦) |
43 | | sneq 4187 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝐵) → {𝑦} = {(𝐹‘𝐵)}) |
44 | 43 | imaeq2d 5466 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)})) |
45 | 44, 19 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → (◡(𝑊‘𝐵) “ {𝑦}) = 𝐶) |
46 | 45 | fveq2d 6195 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = (𝐹‘𝐶)) |
47 | | id 22 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → 𝑦 = (𝐹‘𝐵)) |
48 | 46, 47 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → ((𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦 ↔ (𝐹‘𝐶) = (𝐹‘𝐵))) |
49 | 48 | rspcv 3305 |
. . . 4
⊢ ((𝐹‘𝐵) ∈ 𝐵 → (∀𝑦 ∈ 𝐵 (𝐹‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦 → (𝐹‘𝐶) = (𝐹‘𝐵))) |
50 | 28, 42, 49 | sylc 65 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐶) = (𝐹‘𝐵)) |
51 | 50 | eqcomd 2628 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐹‘𝐵) = (𝐹‘𝐶)) |
52 | 18, 41, 51 | 3jca 1242 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) |