Step | Hyp | Ref
| Expression |
1 | | fpwwe2lem9.m |
. . . 4
⊢ 𝑀 = OrdIso(𝑅, 𝑋) |
2 | 1 | oif 8724 |
. . 3
⊢ 𝑀:dom 𝑀⟶𝑋 |
3 | | ffn 6291 |
. . 3
⊢ (𝑀:dom 𝑀⟶𝑋 → 𝑀 Fn dom 𝑀) |
4 | 2, 3 | mp1i 13 |
. 2
⊢ (𝜑 → 𝑀 Fn dom 𝑀) |
5 | | fpwwe2lem9.n |
. . . . 5
⊢ 𝑁 = OrdIso(𝑆, 𝑌) |
6 | 5 | oif 8724 |
. . . 4
⊢ 𝑁:dom 𝑁⟶𝑌 |
7 | | ffn 6291 |
. . . 4
⊢ (𝑁:dom 𝑁⟶𝑌 → 𝑁 Fn dom 𝑁) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (𝜑 → 𝑁 Fn dom 𝑁) |
9 | | fpwwe2lem9.s |
. . 3
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) |
10 | | fnssres 6250 |
. . 3
⊢ ((𝑁 Fn dom 𝑁 ∧ dom 𝑀 ⊆ dom 𝑁) → (𝑁 ↾ dom 𝑀) Fn dom 𝑀) |
11 | 8, 9, 10 | syl2anc 579 |
. 2
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Fn dom 𝑀) |
12 | 1 | oicl 8723 |
. . . . . 6
⊢ Ord dom
𝑀 |
13 | | ordelon 6000 |
. . . . . 6
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ On) |
14 | 12, 13 | mpan 680 |
. . . . 5
⊢ (𝑤 ∈ dom 𝑀 → 𝑤 ∈ On) |
15 | | eleq1w 2842 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ dom 𝑀 ↔ 𝑦 ∈ dom 𝑀)) |
16 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑀‘𝑤) = (𝑀‘𝑦)) |
17 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑁‘𝑤) = (𝑁‘𝑦)) |
18 | 16, 17 | eqeq12d 2793 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑀‘𝑤) = (𝑁‘𝑤) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) |
19 | 15, 18 | imbi12d 336 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)) ↔ (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) |
20 | 19 | imbi2d 332 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) ↔ (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))))) |
21 | | r19.21v 3142 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) ↔ (𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) |
22 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Ord dom 𝑀) |
23 | | ordelss 5992 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) |
24 | 22, 23 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) |
25 | 24 | sselda 3821 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → 𝑦 ∈ dom 𝑀) |
26 | | pm2.27 42 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ dom 𝑀 → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) |
28 | 27 | ralimdva 3144 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) |
29 | | fnssres 6250 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 Fn dom 𝑀 ∧ 𝑤 ⊆ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) |
30 | 4, 24, 29 | syl2an2r 675 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) |
31 | 9 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → dom 𝑀 ⊆ dom 𝑁) |
32 | 24, 31 | sstrd 3831 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑁) |
33 | | fnssres 6250 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 Fn dom 𝑁 ∧ 𝑤 ⊆ dom 𝑁) → (𝑁 ↾ 𝑤) Fn 𝑤) |
34 | 8, 32, 33 | syl2an2r 675 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁 ↾ 𝑤) Fn 𝑤) |
35 | | eqfnfv 6574 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ↾ 𝑤) Fn 𝑤 ∧ (𝑁 ↾ 𝑤) Fn 𝑤) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) |
36 | 30, 34, 35 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) |
37 | | fvres 6465 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑀 ↾ 𝑤)‘𝑦) = (𝑀‘𝑦)) |
38 | | fvres 6465 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑁 ↾ 𝑤)‘𝑦) = (𝑁‘𝑦)) |
39 | 37, 38 | eqeq12d 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑤 → (((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) |
40 | 39 | ralbiia 3161 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦)) |
41 | 36, 40 | syl6bb 279 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) |
42 | | fpwwe2.1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} |
43 | | fpwwe2.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ V) |
44 | 43 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝐴 ∈ V) |
45 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝜑) |
46 | | fpwwe2.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
47 | 45, 46 | sylan 575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) |
48 | | fpwwe2lem9.x |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋𝑊𝑅) |
49 | 48 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑋𝑊𝑅) |
50 | | fpwwe2lem9.y |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑌𝑊𝑆) |
51 | 50 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑌𝑊𝑆) |
52 | | simplr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑀) |
53 | 9 | sselda 3821 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ dom 𝑁) |
54 | 53 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑁) |
55 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) |
56 | 42, 44, 47, 49, 51, 1, 5, 52, 54, 55 | fpwwe2lem7 9793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑦𝑆(𝑁‘𝑤) ∧ (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)))) |
57 | 56 | simpld 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → 𝑦𝑆(𝑁‘𝑤)) |
58 | 55 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁 ↾ 𝑤) = (𝑀 ↾ 𝑤)) |
59 | 42, 44, 47, 51, 49, 5, 1, 54, 52, 58 | fpwwe2lem7 9793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → (𝑦𝑅(𝑀‘𝑤) ∧ (𝑧𝑆(𝑁‘𝑤) → (𝑦𝑆𝑧 ↔ 𝑦𝑅𝑧)))) |
60 | 59 | simpld 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → 𝑦𝑅(𝑀‘𝑤)) |
61 | 57, 60 | impbida 791 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦𝑅(𝑀‘𝑤) ↔ 𝑦𝑆(𝑁‘𝑤))) |
62 | | fvex 6459 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝑤) ∈ V |
63 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
64 | 63 | eliniseg 5748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀‘𝑤) ∈ V → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤))) |
65 | 62, 64 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤)) |
66 | | fvex 6459 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁‘𝑤) ∈ V |
67 | 63 | eliniseg 5748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁‘𝑤) ∈ V → (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤))) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤)) |
69 | 61, 65, 68 | 3bitr4g 306 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}))) |
70 | 69 | eqrdv 2776 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (◡𝑅 “ {(𝑀‘𝑤)}) = (◡𝑆 “ {(𝑁‘𝑤)})) |
71 | | relinxp 5485 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) |
72 | | relinxp 5485 |
. . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) |
73 | | vex 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑧 ∈ V |
74 | 73 | eliniseg 5748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀‘𝑤) ∈ V → (𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑧𝑅(𝑀‘𝑤))) |
75 | 64, 74 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀‘𝑤) ∈ V → ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤)))) |
76 | 62, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) |
77 | 56 | simprd 491 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧))) |
78 | 77 | impr 448 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
79 | 76, 78 | sylan2b 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) |
80 | 79 | pm5.32da 574 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧))) |
81 | | df-br 4887 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
82 | | brinxp2 5426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) |
83 | 81, 82 | bitr3i 269 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) |
84 | | df-br 4887 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
85 | | brinxp2 5426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) |
86 | 84, 85 | bitr3i 269 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) |
87 | 80, 83, 86 | 3bitr4g 306 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))))) |
88 | 71, 72, 87 | eqrelrdv 5463 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) |
89 | 70 | sqxpeqd 5387 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) = ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))) |
90 | 89 | ineq2d 4037 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) |
91 | 88, 90 | eqtrd 2814 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) |
92 | 70, 91 | oveq12d 6940 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))))) |
93 | 2 | ffvelrni 6622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) ∈ 𝑋) |
94 | 93 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) ∈ 𝑋) |
95 | 94 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) ∈ 𝑋) |
96 | 42, 43, 48 | fpwwe2lem3 9790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑀‘𝑤) ∈ 𝑋) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) |
97 | 45, 95, 96 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) |
98 | 6 | ffvelrni 6622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑁 → (𝑁‘𝑤) ∈ 𝑌) |
99 | 53, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁‘𝑤) ∈ 𝑌) |
100 | 99 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁‘𝑤) ∈ 𝑌) |
101 | 42, 43, 50 | fpwwe2lem3 9790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑁‘𝑤) ∈ 𝑌) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) |
102 | 45, 100, 101 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) |
103 | 92, 97, 102 | 3eqtr3d 2822 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) = (𝑁‘𝑤)) |
104 | 103 | ex 403 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
105 | 41, 104 | sylbird 252 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
106 | 28, 105 | syld 47 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤))) |
107 | 106 | ex 403 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
108 | 107 | com23 86 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
109 | 108 | a2i 14 |
. . . . . . . . 9
⊢ ((𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
110 | 21, 109 | sylbi 209 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
111 | 110 | a1i 11 |
. . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑦 ∈ 𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))))) |
112 | 20, 111 | tfis2 7334 |
. . . . . 6
⊢ (𝑤 ∈ On → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
113 | 112 | com3l 89 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑤 ∈ On → (𝑀‘𝑤) = (𝑁‘𝑤)))) |
114 | 14, 113 | mpdi 45 |
. . . 4
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) |
115 | 114 | imp 397 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = (𝑁‘𝑤)) |
116 | | fvres 6465 |
. . . 4
⊢ (𝑤 ∈ dom 𝑀 → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) |
117 | 116 | adantl 475 |
. . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) |
118 | 115, 117 | eqtr4d 2817 |
. 2
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = ((𝑁 ↾ dom 𝑀)‘𝑤)) |
119 | 4, 11, 118 | eqfnfvd 6577 |
1
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |