Proof of Theorem canthwelem
Step | Hyp | Ref
| Expression |
1 | | eqid 2818 |
. . . . . . . 8
⊢ 𝐵 = 𝐵 |
2 | | eqid 2818 |
. . . . . . . 8
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) |
3 | 1, 2 | pm3.2i 471 |
. . . . . . 7
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) |
4 | | canthwe.2 |
. . . . . . . 8
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
5 | | elex 3510 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
6 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐴 ∈ V) |
7 | | df-ov 7148 |
. . . . . . . . 9
⊢ (𝑥𝐹𝑟) = (𝐹‘〈𝑥, 𝑟〉) |
8 | | f1f 6568 |
. . . . . . . . . . 11
⊢ (𝐹:𝑂–1-1→𝐴 → 𝐹:𝑂⟶𝐴) |
9 | 8 | ad2antlr 723 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → 𝐹:𝑂⟶𝐴) |
10 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) |
11 | | opabidw 5403 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑟〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) |
12 | 10, 11 | sylibr 235 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → 〈𝑥, 𝑟〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}) |
13 | | canthwe.1 |
. . . . . . . . . . 11
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} |
14 | 12, 13 | eleqtrrdi 2921 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → 〈𝑥, 𝑟〉 ∈ 𝑂) |
15 | 9, 14 | ffvelrnd 6844 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹‘〈𝑥, 𝑟〉) ∈ 𝐴) |
16 | 7, 15 | eqeltrid 2914 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
17 | | canthwe.3 |
. . . . . . . 8
⊢ 𝐵 = ∪
dom 𝑊 |
18 | 4, 6, 16, 17 | fpwwe2 10053 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) |
19 | 3, 18 | mpbiri 259 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵)) |
20 | 19 | simprd 496 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) |
21 | | canthwe.4 |
. . . . . . . . . 10
⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) |
22 | 21, 21 | xpeq12i 5576 |
. . . . . . . . . . 11
⊢ (𝐶 × 𝐶) = ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})) |
23 | 22 | ineq2i 4183 |
. . . . . . . . . 10
⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) = ((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}))) |
24 | 21, 23 | oveq12i 7157 |
. . . . . . . . 9
⊢ (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))) |
25 | 19 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵𝑊(𝑊‘𝐵)) |
26 | 4, 6, 25 | fpwwe2lem3 10043 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) → ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))) = (𝐵𝐹(𝑊‘𝐵))) |
27 | 20, 26 | mpdan 683 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})𝐹((𝑊‘𝐵) ∩ ((◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) × (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})))) = (𝐵𝐹(𝑊‘𝐵))) |
28 | 24, 27 | syl5eq 2865 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = (𝐵𝐹(𝑊‘𝐵))) |
29 | | df-ov 7148 |
. . . . . . . 8
⊢ (𝐶𝐹((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) = (𝐹‘〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉) |
30 | | df-ov 7148 |
. . . . . . . 8
⊢ (𝐵𝐹(𝑊‘𝐵)) = (𝐹‘〈𝐵, (𝑊‘𝐵)〉) |
31 | 28, 29, 30 | 3eqtr3g 2876 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐹‘〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉) = (𝐹‘〈𝐵, (𝑊‘𝐵)〉)) |
32 | | simpr 485 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐹:𝑂–1-1→𝐴) |
33 | | cnvimass 5942 |
. . . . . . . . . . . . 13
⊢ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⊆ dom (𝑊‘𝐵) |
34 | 4, 6 | fpwwe2lem2 10042 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦)))) |
35 | 25, 34 | mpbid 233 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦))) |
36 | 35 | simpld 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))) |
37 | 36 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) |
38 | | dmss 5764 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊‘𝐵) ⊆ (𝐵 × 𝐵) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → dom (𝑊‘𝐵) ⊆ dom (𝐵 × 𝐵)) |
40 | | dmxpss 6021 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐵 × 𝐵) ⊆ 𝐵 |
41 | 39, 40 | sstrdi 3976 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → dom (𝑊‘𝐵) ⊆ 𝐵) |
42 | 33, 41 | sstrid 3975 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⊆ 𝐵) |
43 | 21, 42 | eqsstrid 4012 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 ⊆ 𝐵) |
44 | 36 | simpld 495 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵 ⊆ 𝐴) |
45 | 43, 44 | sstrd 3974 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 ⊆ 𝐴) |
46 | | inss2 4203 |
. . . . . . . . . . 11
⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶)) |
48 | 35 | simprd 496 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 [(◡(𝑊‘𝐵) “ {𝑦}) / 𝑢](𝑢𝐹((𝑊‘𝐵) ∩ (𝑢 × 𝑢))) = 𝑦)) |
49 | 48 | simpld 495 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) We 𝐵) |
50 | | wess 5535 |
. . . . . . . . . . . 12
⊢ (𝐶 ⊆ 𝐵 → ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) We 𝐶)) |
51 | 43, 49, 50 | sylc 65 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) We 𝐶) |
52 | | weinxp 5629 |
. . . . . . . . . . 11
⊢ ((𝑊‘𝐵) We 𝐶 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶) |
53 | 51, 52 | sylib 219 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶) |
54 | | fvex 6676 |
. . . . . . . . . . . . . 14
⊢ (𝑊‘𝐵) ∈ V |
55 | 54 | cnvex 7619 |
. . . . . . . . . . . . 13
⊢ ◡(𝑊‘𝐵) ∈ V |
56 | 55 | imaex 7610 |
. . . . . . . . . . . 12
⊢ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ∈ V |
57 | 21, 56 | eqeltri 2906 |
. . . . . . . . . . 11
⊢ 𝐶 ∈ V |
58 | 54 | inex1 5212 |
. . . . . . . . . . 11
⊢ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ∈ V |
59 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → 𝑥 = 𝐶) |
60 | 59 | sseq1d 3995 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑥 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐴)) |
61 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) |
62 | 59 | sqxpeqd 5580 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑥 × 𝑥) = (𝐶 × 𝐶)) |
63 | 61, 62 | sseq12d 3997 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶))) |
64 | | weeq2 5537 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐶 → (𝑟 We 𝑥 ↔ 𝑟 We 𝐶)) |
65 | | weeq1 5536 |
. . . . . . . . . . . . 13
⊢ (𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) → (𝑟 We 𝐶 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)) |
66 | 64, 65 | sylan9bb 510 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → (𝑟 We 𝑥 ↔ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)) |
67 | 60, 63, 66 | 3anbi123d 1427 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝐶 ∧ 𝑟 = ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐶 ⊆ 𝐴 ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶))) |
68 | 57, 58, 67 | opelopaba 5414 |
. . . . . . . . . 10
⊢
(〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐶 ⊆ 𝐴 ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) ⊆ (𝐶 × 𝐶) ∧ ((𝑊‘𝐵) ∩ (𝐶 × 𝐶)) We 𝐶)) |
69 | 45, 47, 53, 68 | syl3anbrc 1335 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}) |
70 | 69, 13 | eleqtrrdi 2921 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 ∈ 𝑂) |
71 | 6, 44 | ssexd 5219 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐵 ∈ V) |
72 | 54 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) ∈ V) |
73 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → 𝑥 = 𝐵) |
74 | 73 | sseq1d 3995 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑥 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴)) |
75 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → 𝑟 = (𝑊‘𝐵)) |
76 | 73 | sqxpeqd 5580 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑥 × 𝑥) = (𝐵 × 𝐵)) |
77 | 75, 76 | sseq12d 3997 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵))) |
78 | | weeq2 5537 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐵 → (𝑟 We 𝑥 ↔ 𝑟 We 𝐵)) |
79 | | weeq1 5536 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵)) |
80 | 78, 79 | sylan9bb 510 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → (𝑟 We 𝑥 ↔ (𝑊‘𝐵) We 𝐵)) |
81 | 74, 77, 80 | 3anbi123d 1427 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝐵 ∧ 𝑟 = (𝑊‘𝐵)) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵))) |
82 | 81 | opelopabga 5411 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ (𝑊‘𝐵) ∈ V) → (〈𝐵, (𝑊‘𝐵)〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵))) |
83 | 71, 72, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (〈𝐵, (𝑊‘𝐵)〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ↔ (𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵) ∧ (𝑊‘𝐵) We 𝐵))) |
84 | 44, 37, 49, 83 | mpbir3and 1334 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 〈𝐵, (𝑊‘𝐵)〉 ∈ {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)}) |
85 | 84, 13 | eleqtrrdi 2921 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 〈𝐵, (𝑊‘𝐵)〉 ∈ 𝑂) |
86 | | f1fveq 7011 |
. . . . . . . 8
⊢ ((𝐹:𝑂–1-1→𝐴 ∧ (〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 ∈ 𝑂 ∧ 〈𝐵, (𝑊‘𝐵)〉 ∈ 𝑂)) → ((𝐹‘〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉) = (𝐹‘〈𝐵, (𝑊‘𝐵)〉) ↔ 〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 = 〈𝐵, (𝑊‘𝐵)〉)) |
87 | 32, 70, 85, 86 | syl12anc 832 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐹‘〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉) = (𝐹‘〈𝐵, (𝑊‘𝐵)〉) ↔ 〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 = 〈𝐵, (𝑊‘𝐵)〉)) |
88 | 31, 87 | mpbid 233 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 = 〈𝐵, (𝑊‘𝐵)〉) |
89 | 57, 58 | opth1 5358 |
. . . . . 6
⊢
(〈𝐶, ((𝑊‘𝐵) ∩ (𝐶 × 𝐶))〉 = 〈𝐵, (𝑊‘𝐵)〉 → 𝐶 = 𝐵) |
90 | 88, 89 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → 𝐶 = 𝐵) |
91 | 20, 90 | eleqtrrd 2913 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐶) |
92 | 91, 21 | eleqtrdi 2920 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))})) |
93 | | ovex 7178 |
. . . . 5
⊢ (𝐵𝐹(𝑊‘𝐵)) ∈ V |
94 | 93 | eliniseg 5951 |
. . . 4
⊢ ((𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵 → ((𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ↔ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵)))) |
95 | 20, 94 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ((𝐵𝐹(𝑊‘𝐵)) ∈ (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ↔ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵)))) |
96 | 92, 95 | mpbid 233 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵))) |
97 | | weso 5539 |
. . . 4
⊢ ((𝑊‘𝐵) We 𝐵 → (𝑊‘𝐵) Or 𝐵) |
98 | 49, 97 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → (𝑊‘𝐵) Or 𝐵) |
99 | | sonr 5489 |
. . 3
⊢ (((𝑊‘𝐵) Or 𝐵 ∧ (𝐵𝐹(𝑊‘𝐵)) ∈ 𝐵) → ¬ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵))) |
100 | 98, 20, 99 | syl2anc 584 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝑂–1-1→𝐴) → ¬ (𝐵𝐹(𝑊‘𝐵))(𝑊‘𝐵)(𝐵𝐹(𝑊‘𝐵))) |
101 | 96, 100 | pm2.65da 813 |
1
⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴) |