Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.m |
. . . 4
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
2 | 1 | oif 8318 |
. . 3
⊢ 𝑀:dom 𝑀⟶𝑋 |
3 | | ffn 5958 |
. . 3
⊢ (𝑀:dom 𝑀⟶𝑋 → 𝑀 Fn dom 𝑀) |
4 | 2, 3 | mp1i 13 |
. 2
⊢ (𝜑 → 𝑀 Fn dom 𝑀) |
5 | | fpwwe2lem9.n |
. . . . 5
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
6 | 5 | oif 8318 |
. . . 4
⊢ 𝑁:dom 𝑁⟶𝑌 |
7 | | ffn 5958 |
. . . 4
⊢ (𝑁:dom 𝑁⟶𝑌 → 𝑁 Fn dom 𝑁) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (𝜑 → 𝑁 Fn dom 𝑁) |
9 | | fpwwe2lem9.s |
. . 3
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) |
10 | | fnssres 5918 |
. . 3
⊢ ((𝑁 Fn dom 𝑁 ∧ dom 𝑀 ⊆ dom 𝑁) → (𝑁 ↾ dom 𝑀) Fn dom 𝑀) |
11 | 8, 9, 10 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Fn dom 𝑀) |
12 | 1 | oicl 8317 |
. . . . . 6
⊢ Ord dom
𝑀 |
13 | | ordelon 5664 |
. . . . . 6
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ On) |
14 | 12, 13 | mpan 702 |
. . . . 5
⊢ (𝑤 ∈ dom 𝑀 → 𝑤 ∈ On) |
15 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ dom 𝑀 ↔ 𝑦 ∈ dom 𝑀)) |
16 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑀‘𝑤) = (𝑀‘𝑦)) |
17 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑁‘𝑤) = (𝑁‘𝑦)) |
18 | 16, 17 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑀‘𝑤) = (𝑁‘𝑤) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) |
19 | 15, 18 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)) ↔ (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) |
20 | 19 | imbi2d 329 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) ↔ (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))))) |
21 | | r19.21v 2943 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) ↔ (𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) |
22 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Ord dom 𝑀) |
23 | | ordelss 5656 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) |
24 | 22, 23 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) |
25 | 24 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → 𝑦 ∈ dom 𝑀) |
26 | | pm2.27 41 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ dom 𝑀 → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) |
28 | 27 | ralimdva 2945 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) |
29 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑀 Fn dom 𝑀) |
30 | | fnssres 5918 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 Fn dom 𝑀 ∧ 𝑤 ⊆ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) |
31 | 29, 24, 30 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) |
32 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑁 Fn dom 𝑁) |
33 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → dom 𝑀 ⊆ dom 𝑁) |
34 | 24, 33 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑁) |
35 | | fnssres 5918 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 Fn dom 𝑁 ∧ 𝑤 ⊆ dom 𝑁) → (𝑁 ↾ 𝑤) Fn 𝑤) |
36 | 32, 34, 35 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁 ↾ 𝑤) Fn 𝑤) |
37 | | eqfnfv 6219 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ↾ 𝑤) Fn 𝑤 ∧ (𝑁 ↾ 𝑤) Fn 𝑤) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) |
38 | 31, 36, 37 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) |
39 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑀 ↾ 𝑤)‘𝑦) = (𝑀‘𝑦)) |
40 | | fvres 6117 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑁 ↾ 𝑤)‘𝑦) = (𝑁‘𝑦)) |
41 | 39, 40 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑤 → (((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) |
42 | 41 | ralbiia 2962 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦)) |
43 | 38, 42 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) |
44 | | fpwwe2.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
45 | | fpwwe2.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ V) |
46 | 45 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝐴 ∈ V) |
47 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝜑) |
48 | | fpwwe2.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
49 | 47, 48 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
50 | | fpwwe2lem9.x |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋𝑊𝑅) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑋𝑊𝑅) |
52 | | fpwwe2lem9.y |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑌𝑊𝑆) |
53 | 52 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑌𝑊𝑆) |
54 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑀) |
55 | 9 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ dom 𝑁) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑁) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) |
58 | 44, 46, 49, 51, 53, 1, 5, 54, 56, 57 | fpwwe2lem7 9337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑦𝑆(𝑁‘𝑤) ∧ (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)))) |
59 | 58 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → 𝑦𝑆(𝑁‘𝑤)) |
60 | 57 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁 ↾ 𝑤) = (𝑀 ↾ 𝑤)) |
61 | 44, 46, 49, 53, 51, 5, 1, 56, 54, 60 | fpwwe2lem7 9337 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → (𝑦𝑅(𝑀‘𝑤) ∧ (𝑧𝑆(𝑁‘𝑤) → (𝑦𝑆𝑧 ↔ 𝑦𝑅𝑧)))) |
62 | 61 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → 𝑦𝑅(𝑀‘𝑤)) |
63 | 59, 62 | impbida 873 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦𝑅(𝑀‘𝑤) ↔ 𝑦𝑆(𝑁‘𝑤))) |
64 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝑤) ∈ V |
65 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
66 | 65 | eliniseg 5413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀‘𝑤) ∈ V → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤))) |
67 | 64, 66 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤)) |
68 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁‘𝑤) ∈ V |
69 | 65 | eliniseg 5413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁‘𝑤) ∈ V → (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤))) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤)) |
71 | 63, 67, 70 | 3bitr4g 302 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}))) |
72 | 71 | eqrdv 2608 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (◡𝑅 “ {(𝑀‘𝑤)}) = (◡𝑆 “ {(𝑁‘𝑤)})) |
73 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ⊆ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) |
74 | | relxp 5150 |
. . . . . . . . . . . . . . . . . . . 20
⊢ Rel
((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) |
75 | | relss 5129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ⊆ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) → (Rel ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) → Rel (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))))) |
76 | 73, 74, 75 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) |
77 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ⊆ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) |
78 | | relss 5129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ⊆ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) → (Rel ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) → Rel (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))))) |
79 | 77, 74, 78 | mp2 9 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) |
80 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑧 ∈ V |
81 | 80 | eliniseg 5413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀‘𝑤) ∈ V → (𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑧𝑅(𝑀‘𝑤))) |
82 | 66, 81 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀‘𝑤) ∈ V → ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤)))) |
83 | 64, 82 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) |
84 | 58 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧))) |
85 | 84 | impr 647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
86 | 83, 85 | sylan2b 491 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
87 | 86 | pm5.32da 671 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧))) |
88 | | brinxp2 5103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑦𝑅𝑧)) |
89 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
90 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) |
91 | 88, 89, 90 | 3bitr3i 289 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) |
92 | | brinxp2 5103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑦𝑆𝑧)) |
93 | | df-br 4584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
94 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑦𝑆𝑧) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) |
95 | 92, 93, 94 | 3bitr3i 289 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) |
96 | 87, 91, 95 | 3bitr4g 302 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))))) |
97 | 76, 79, 96 | eqrelrdv 5139 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
98 | 72 | sqxpeqd 5065 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) = ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))) |
99 | 98 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) |
100 | 97, 99 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) |
101 | 72, 100 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))))) |
102 | 2 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) ∈ 𝑋) |
103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) ∈ 𝑋) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) ∈ 𝑋) |
105 | 44, 45, 50 | fpwwe2lem3 9334 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑀‘𝑤) ∈ 𝑋) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) |
106 | 47, 104, 105 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) |
107 | 6 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑁 → (𝑁‘𝑤) ∈ 𝑌) |
108 | 55, 107 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁‘𝑤) ∈ 𝑌) |
109 | 108 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁‘𝑤) ∈ 𝑌) |
110 | 44, 45, 52 | fpwwe2lem3 9334 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑁‘𝑤) ∈ 𝑌) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) |
111 | 47, 109, 110 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) |
112 | 101, 106,
111 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) = (𝑁‘𝑤)) |
113 | 112 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
114 | 43, 113 | sylbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
115 | 28, 114 | syld 46 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
116 | 115 | ex 449 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
117 | 116 | com23 84 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
118 | 117 | a2i 14 |
. . . . . . . . 9
⊢ ((𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
119 | 21, 118 | sylbi 206 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑦 ∈ 𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))))) |
121 | 20, 120 | tfis2 6948 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
122 | 121 | com3l 87 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑤 ∈ On → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
123 | 14, 122 | mpdi 44 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) |
124 | 123 | imp 444 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = (𝑁‘𝑤)) |
125 | | fvres 6117 |
. . . 4
⊢ (𝑤 ∈ dom 𝑀 → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) |
126 | 125 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) |
127 | 124, 126 | eqtr4d 2647 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = ((𝑁 ↾ dom 𝑀)‘𝑤)) |
128 | 4, 11, 127 | eqfnfvd 6222 |
1
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |