| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fpwwe2lem8.m | . . . 4
⊢ 𝑀 = OrdIso(𝑅, 𝑋) | 
| 2 | 1 | oif 9571 | . . 3
⊢ 𝑀:dom 𝑀⟶𝑋 | 
| 3 |  | ffn 6735 | . . 3
⊢ (𝑀:dom 𝑀⟶𝑋 → 𝑀 Fn dom 𝑀) | 
| 4 | 2, 3 | mp1i 13 | . 2
⊢ (𝜑 → 𝑀 Fn dom 𝑀) | 
| 5 |  | fpwwe2lem8.n | . . . . 5
⊢ 𝑁 = OrdIso(𝑆, 𝑌) | 
| 6 | 5 | oif 9571 | . . . 4
⊢ 𝑁:dom 𝑁⟶𝑌 | 
| 7 |  | ffn 6735 | . . . 4
⊢ (𝑁:dom 𝑁⟶𝑌 → 𝑁 Fn dom 𝑁) | 
| 8 | 6, 7 | mp1i 13 | . . 3
⊢ (𝜑 → 𝑁 Fn dom 𝑁) | 
| 9 |  | fpwwe2lem8.s | . . 3
⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) | 
| 10 | 8, 9 | fnssresd 6691 | . 2
⊢ (𝜑 → (𝑁 ↾ dom 𝑀) Fn dom 𝑀) | 
| 11 | 1 | oicl 9570 | . . . . . 6
⊢ Ord dom
𝑀 | 
| 12 |  | ordelon 6407 | . . . . . 6
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ On) | 
| 13 | 11, 12 | mpan 690 | . . . . 5
⊢ (𝑤 ∈ dom 𝑀 → 𝑤 ∈ On) | 
| 14 |  | eleq1w 2823 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 ∈ dom 𝑀 ↔ 𝑦 ∈ dom 𝑀)) | 
| 15 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑀‘𝑤) = (𝑀‘𝑦)) | 
| 16 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑁‘𝑤) = (𝑁‘𝑦)) | 
| 17 | 15, 16 | eqeq12d 2752 | . . . . . . . . 9
⊢ (𝑤 = 𝑦 → ((𝑀‘𝑤) = (𝑁‘𝑤) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 18 | 14, 17 | imbi12d 344 | . . . . . . . 8
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)) ↔ (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) | 
| 19 | 18 | imbi2d 340 | . . . . . . 7
⊢ (𝑤 = 𝑦 → ((𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) ↔ (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))))) | 
| 20 |  | r19.21v 3179 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) ↔ (𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)))) | 
| 21 | 11 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Ord dom 𝑀) | 
| 22 |  | ordelss 6399 | . . . . . . . . . . . . . . . . 17
⊢ ((Ord dom
𝑀 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) | 
| 23 | 21, 22 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀) | 
| 24 | 23 | sselda 3982 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → 𝑦 ∈ dom 𝑀) | 
| 25 |  | pm2.27 42 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ dom 𝑀 → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 26 | 24, 25 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ 𝑦 ∈ 𝑤) → ((𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 27 | 26 | ralimdva 3166 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 28 |  | fnssres 6690 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑀 Fn dom 𝑀 ∧ 𝑤 ⊆ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) | 
| 29 | 4, 23, 28 | syl2an2r 685 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀 ↾ 𝑤) Fn 𝑤) | 
| 30 | 9 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → dom 𝑀 ⊆ dom 𝑁) | 
| 31 | 23, 30 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑁) | 
| 32 |  | fnssres 6690 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 Fn dom 𝑁 ∧ 𝑤 ⊆ dom 𝑁) → (𝑁 ↾ 𝑤) Fn 𝑤) | 
| 33 | 8, 31, 32 | syl2an2r 685 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁 ↾ 𝑤) Fn 𝑤) | 
| 34 |  | eqfnfv 7050 | . . . . . . . . . . . . . . . 16
⊢ (((𝑀 ↾ 𝑤) Fn 𝑤 ∧ (𝑁 ↾ 𝑤) Fn 𝑤) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) | 
| 35 | 29, 33, 34 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦))) | 
| 36 |  | fvres 6924 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑀 ↾ 𝑤)‘𝑦) = (𝑀‘𝑦)) | 
| 37 |  | fvres 6924 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝑤 → ((𝑁 ↾ 𝑤)‘𝑦) = (𝑁‘𝑦)) | 
| 38 | 36, 37 | eqeq12d 2752 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑤 → (((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 39 | 38 | ralbiia 3090 | . . . . . . . . . . . . . . 15
⊢
(∀𝑦 ∈
𝑤 ((𝑀 ↾ 𝑤)‘𝑦) = ((𝑁 ↾ 𝑤)‘𝑦) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦)) | 
| 40 | 35, 39 | bitrdi 287 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) ↔ ∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦))) | 
| 41 |  | fpwwe2.1 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} | 
| 42 |  | fpwwe2.2 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 43 | 42 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝐴 ∈ 𝑉) | 
| 44 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝜑) | 
| 45 |  | fpwwe2.3 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) | 
| 46 | 44, 45 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) | 
| 47 |  | fpwwe2lem8.x | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑋𝑊𝑅) | 
| 48 | 47 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑋𝑊𝑅) | 
| 49 |  | fpwwe2lem8.y | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑌𝑊𝑆) | 
| 50 | 49 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑌𝑊𝑆) | 
| 51 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑀) | 
| 52 | 9 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → 𝑤 ∈ dom 𝑁) | 
| 53 | 52 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → 𝑤 ∈ dom 𝑁) | 
| 54 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) | 
| 55 | 41, 43, 46, 48, 50, 1, 5, 51, 53, 54 | fpwwe2lem6 10677 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑦𝑆(𝑁‘𝑤) ∧ (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)))) | 
| 56 | 55 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → 𝑦𝑆(𝑁‘𝑤)) | 
| 57 | 54 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁 ↾ 𝑤) = (𝑀 ↾ 𝑤)) | 
| 58 | 41, 43, 46, 50, 48, 5, 1, 53, 51, 57 | fpwwe2lem6 10677 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → (𝑦𝑅(𝑀‘𝑤) ∧ (𝑧𝑆(𝑁‘𝑤) → (𝑦𝑆𝑧 ↔ 𝑦𝑅𝑧)))) | 
| 59 | 58 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑆(𝑁‘𝑤)) → 𝑦𝑅(𝑀‘𝑤)) | 
| 60 | 56, 59 | impbida 800 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦𝑅(𝑀‘𝑤) ↔ 𝑦𝑆(𝑁‘𝑤))) | 
| 61 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝑤) ∈ V | 
| 62 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V | 
| 63 | 62 | eliniseg 6111 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀‘𝑤) ∈ V → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤))) | 
| 64 | 61, 63 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦𝑅(𝑀‘𝑤)) | 
| 65 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁‘𝑤) ∈ V | 
| 66 | 62 | eliniseg 6111 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁‘𝑤) ∈ V → (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤))) | 
| 67 | 65, 66 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}) ↔ 𝑦𝑆(𝑁‘𝑤)) | 
| 68 | 60, 64, 67 | 3bitr4g 314 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑦 ∈ (◡𝑆 “ {(𝑁‘𝑤)}))) | 
| 69 | 68 | eqrdv 2734 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (◡𝑅 “ {(𝑀‘𝑤)}) = (◡𝑆 “ {(𝑁‘𝑤)})) | 
| 70 |  | relinxp 5823 | . . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) | 
| 71 |  | relinxp 5823 | . . . . . . . . . . . . . . . . . . 19
⊢ Rel
(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) | 
| 72 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑧 ∈ V | 
| 73 | 72 | eliniseg 6111 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀‘𝑤) ∈ V → (𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ↔ 𝑧𝑅(𝑀‘𝑤))) | 
| 74 | 63, 73 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀‘𝑤) ∈ V → ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤)))) | 
| 75 | 61, 74 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ↔ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) | 
| 76 | 55 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ 𝑦𝑅(𝑀‘𝑤)) → (𝑧𝑅(𝑀‘𝑤) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧))) | 
| 77 | 76 | impr 454 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦𝑅(𝑀‘𝑤) ∧ 𝑧𝑅(𝑀‘𝑤))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) | 
| 78 | 75, 77 | sylan2b 594 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) ∧ (𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)}))) → (𝑦𝑅𝑧 ↔ 𝑦𝑆𝑧)) | 
| 79 | 78 | pm5.32da 579 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧))) | 
| 80 |  | df-br 5143 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) | 
| 81 |  | brinxp2 5762 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) | 
| 82 | 80, 81 | bitr3i 277 | . . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑅𝑧)) | 
| 83 |  | df-br 5143 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) | 
| 84 |  | brinxp2 5762 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦(𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))𝑧 ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) | 
| 85 | 83, 84 | bitr3i 277 | . . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ ((𝑦 ∈ (◡𝑅 “ {(𝑀‘𝑤)}) ∧ 𝑧 ∈ (◡𝑅 “ {(𝑀‘𝑤)})) ∧ 𝑦𝑆𝑧)) | 
| 86 | 79, 82, 85 | 3bitr4g 314 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (〈𝑦, 𝑧〉 ∈ (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) ↔ 〈𝑦, 𝑧〉 ∈ (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))))) | 
| 87 | 70, 71, 86 | eqrelrdv 5801 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) | 
| 88 | 69 | sqxpeqd 5716 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})) = ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))) | 
| 89 | 88 | ineq2d 4219 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑆 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) | 
| 90 | 87, 89 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)}))) = (𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) | 
| 91 | 69, 90 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)}))))) | 
| 92 | 2 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) ∈ 𝑋) | 
| 93 | 92 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) ∈ 𝑋) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) ∈ 𝑋) | 
| 95 | 41, 42, 47 | fpwwe2lem3 10674 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑀‘𝑤) ∈ 𝑋) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) | 
| 96 | 44, 94, 95 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑅 “ {(𝑀‘𝑤)})𝐹(𝑅 ∩ ((◡𝑅 “ {(𝑀‘𝑤)}) × (◡𝑅 “ {(𝑀‘𝑤)})))) = (𝑀‘𝑤)) | 
| 97 | 6 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ dom 𝑁 → (𝑁‘𝑤) ∈ 𝑌) | 
| 98 | 52, 97 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑁‘𝑤) ∈ 𝑌) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑁‘𝑤) ∈ 𝑌) | 
| 100 | 41, 42, 49 | fpwwe2lem3 10674 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑁‘𝑤) ∈ 𝑌) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) | 
| 101 | 44, 99, 100 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → ((◡𝑆 “ {(𝑁‘𝑤)})𝐹(𝑆 ∩ ((◡𝑆 “ {(𝑁‘𝑤)}) × (◡𝑆 “ {(𝑁‘𝑤)})))) = (𝑁‘𝑤)) | 
| 102 | 91, 96, 101 | 3eqtr3d 2784 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ dom 𝑀) ∧ (𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤)) → (𝑀‘𝑤) = (𝑁‘𝑤)) | 
| 103 | 102 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑀 ↾ 𝑤) = (𝑁 ↾ 𝑤) → (𝑀‘𝑤) = (𝑁‘𝑤))) | 
| 104 | 40, 103 | sylbird 260 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑀‘𝑦) = (𝑁‘𝑦) → (𝑀‘𝑤) = (𝑁‘𝑤))) | 
| 105 | 27, 104 | syld 47 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤))) | 
| 106 | 105 | ex 412 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 107 | 106 | com23 86 | . . . . . . . . . 10
⊢ (𝜑 → (∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦)) → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 108 | 107 | a2i 14 | . . . . . . . . 9
⊢ ((𝜑 → ∀𝑦 ∈ 𝑤 (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 109 | 20, 108 | sylbi 217 | . . . . . . . 8
⊢
(∀𝑦 ∈
𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 110 | 109 | a1i 11 | . . . . . . 7
⊢ (𝑤 ∈ On → (∀𝑦 ∈ 𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀‘𝑦) = (𝑁‘𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))))) | 
| 111 | 19, 110 | tfis2 7879 | . . . . . 6
⊢ (𝑤 ∈ On → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 112 | 111 | com3l 89 | . . . . 5
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑤 ∈ On → (𝑀‘𝑤) = (𝑁‘𝑤)))) | 
| 113 | 13, 112 | mpdi 45 | . . . 4
⊢ (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀‘𝑤) = (𝑁‘𝑤))) | 
| 114 | 113 | imp 406 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = (𝑁‘𝑤)) | 
| 115 |  | fvres 6924 | . . . 4
⊢ (𝑤 ∈ dom 𝑀 → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) | 
| 116 | 115 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁‘𝑤)) | 
| 117 | 114, 116 | eqtr4d 2779 | . 2
⊢ ((𝜑 ∧ 𝑤 ∈ dom 𝑀) → (𝑀‘𝑤) = ((𝑁 ↾ dom 𝑀)‘𝑤)) | 
| 118 | 4, 10, 117 | eqfnfvd 7053 | 1
⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) |