Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2lem8 Structured version   Visualization version   GIF version

Theorem fpwwe2lem8 10057
 Description: Lemma for fpwwe2 10063. Show by induction that the two isometries 𝑀 and 𝑁 agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2lem9.x (𝜑𝑋𝑊𝑅)
fpwwe2lem9.y (𝜑𝑌𝑊𝑆)
fpwwe2lem9.m 𝑀 = OrdIso(𝑅, 𝑋)
fpwwe2lem9.n 𝑁 = OrdIso(𝑆, 𝑌)
fpwwe2lem9.s (𝜑 → dom 𝑀 ⊆ dom 𝑁)
Assertion
Ref Expression
fpwwe2lem8 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem8
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2lem9.m . . . 4 𝑀 = OrdIso(𝑅, 𝑋)
21oif 8991 . . 3 𝑀:dom 𝑀𝑋
3 ffn 6503 . . 3 (𝑀:dom 𝑀𝑋𝑀 Fn dom 𝑀)
42, 3mp1i 13 . 2 (𝜑𝑀 Fn dom 𝑀)
5 fpwwe2lem9.n . . . . 5 𝑁 = OrdIso(𝑆, 𝑌)
65oif 8991 . . . 4 𝑁:dom 𝑁𝑌
7 ffn 6503 . . . 4 (𝑁:dom 𝑁𝑌𝑁 Fn dom 𝑁)
86, 7mp1i 13 . . 3 (𝜑𝑁 Fn dom 𝑁)
9 fpwwe2lem9.s . . 3 (𝜑 → dom 𝑀 ⊆ dom 𝑁)
10 fnssres 6459 . . 3 ((𝑁 Fn dom 𝑁 ∧ dom 𝑀 ⊆ dom 𝑁) → (𝑁 ↾ dom 𝑀) Fn dom 𝑀)
118, 9, 10syl2anc 587 . 2 (𝜑 → (𝑁 ↾ dom 𝑀) Fn dom 𝑀)
121oicl 8990 . . . . . 6 Ord dom 𝑀
13 ordelon 6202 . . . . . 6 ((Ord dom 𝑀𝑤 ∈ dom 𝑀) → 𝑤 ∈ On)
1412, 13mpan 689 . . . . 5 (𝑤 ∈ dom 𝑀𝑤 ∈ On)
15 eleq1w 2898 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤 ∈ dom 𝑀𝑦 ∈ dom 𝑀))
16 fveq2 6661 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑀𝑤) = (𝑀𝑦))
17 fveq2 6661 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑁𝑤) = (𝑁𝑦))
1816, 17eqeq12d 2840 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑀𝑦) = (𝑁𝑦)))
1915, 18imbi12d 348 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)) ↔ (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))))
2019imbi2d 344 . . . . . . 7 (𝑤 = 𝑦 → ((𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))) ↔ (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)))))
21 r19.21v 3170 . . . . . . . . 9 (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) ↔ (𝜑 → ∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))))
2212a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord dom 𝑀)
23 ordelss 6194 . . . . . . . . . . . . . . . . 17 ((Ord dom 𝑀𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀)
2422, 23sylan 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀)
2524sselda 3953 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ dom 𝑀) ∧ 𝑦𝑤) → 𝑦 ∈ dom 𝑀)
26 pm2.27 42 . . . . . . . . . . . . . . 15 (𝑦 ∈ dom 𝑀 → ((𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑦) = (𝑁𝑦)))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ dom 𝑀) ∧ 𝑦𝑤) → ((𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑦) = (𝑁𝑦)))
2827ralimdva 3172 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦)))
29 fnssres 6459 . . . . . . . . . . . . . . . . 17 ((𝑀 Fn dom 𝑀𝑤 ⊆ dom 𝑀) → (𝑀𝑤) Fn 𝑤)
304, 24, 29syl2an2r 684 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) Fn 𝑤)
319adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → dom 𝑀 ⊆ dom 𝑁)
3224, 31sstrd 3963 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑁)
33 fnssres 6459 . . . . . . . . . . . . . . . . 17 ((𝑁 Fn dom 𝑁𝑤 ⊆ dom 𝑁) → (𝑁𝑤) Fn 𝑤)
348, 32, 33syl2an2r 684 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → (𝑁𝑤) Fn 𝑤)
35 eqfnfv 6793 . . . . . . . . . . . . . . . 16 (((𝑀𝑤) Fn 𝑤 ∧ (𝑁𝑤) Fn 𝑤) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦)))
3630, 34, 35syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦)))
37 fvres 6680 . . . . . . . . . . . . . . . . 17 (𝑦𝑤 → ((𝑀𝑤)‘𝑦) = (𝑀𝑦))
38 fvres 6680 . . . . . . . . . . . . . . . . 17 (𝑦𝑤 → ((𝑁𝑤)‘𝑦) = (𝑁𝑦))
3937, 38eqeq12d 2840 . . . . . . . . . . . . . . . 16 (𝑦𝑤 → (((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦) ↔ (𝑀𝑦) = (𝑁𝑦)))
4039ralbiia 3159 . . . . . . . . . . . . . . 15 (∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦) ↔ ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦))
4136, 40syl6bb 290 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦)))
42 fpwwe2.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
43 fpwwe2.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ V)
4443ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝐴 ∈ V)
45 simpll 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝜑)
46 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
4745, 46sylan 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
48 fpwwe2lem9.x . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋𝑊𝑅)
4948ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑋𝑊𝑅)
50 fpwwe2lem9.y . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑌𝑊𝑆)
5150ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑌𝑊𝑆)
52 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑤 ∈ dom 𝑀)
539sselda 3953 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ∈ dom 𝑁)
5453adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑤 ∈ dom 𝑁)
55 simpr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) = (𝑁𝑤))
5642, 44, 47, 49, 51, 1, 5, 52, 54, 55fpwwe2lem7 10056 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → (𝑦𝑆(𝑁𝑤) ∧ (𝑧𝑅(𝑀𝑤) → (𝑦𝑅𝑧𝑦𝑆𝑧))))
5756simpld 498 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → 𝑦𝑆(𝑁𝑤))
5855eqcomd 2830 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑁𝑤) = (𝑀𝑤))
5942, 44, 47, 51, 49, 5, 1, 54, 52, 58fpwwe2lem7 10056 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑆(𝑁𝑤)) → (𝑦𝑅(𝑀𝑤) ∧ (𝑧𝑆(𝑁𝑤) → (𝑦𝑆𝑧𝑦𝑅𝑧))))
6059simpld 498 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑆(𝑁𝑤)) → 𝑦𝑅(𝑀𝑤))
6157, 60impbida 800 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑦𝑅(𝑀𝑤) ↔ 𝑦𝑆(𝑁𝑤)))
62 fvex 6674 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝑤) ∈ V
63 vex 3483 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
6463eliniseg 5945 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑤) ∈ V → (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦𝑅(𝑀𝑤)))
6562, 64ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦𝑅(𝑀𝑤))
66 fvex 6674 . . . . . . . . . . . . . . . . . . . 20 (𝑁𝑤) ∈ V
6763eliniseg 5945 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑤) ∈ V → (𝑦 ∈ (𝑆 “ {(𝑁𝑤)}) ↔ 𝑦𝑆(𝑁𝑤)))
6866, 67ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑆 “ {(𝑁𝑤)}) ↔ 𝑦𝑆(𝑁𝑤))
6961, 65, 683bitr4g 317 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦 ∈ (𝑆 “ {(𝑁𝑤)})))
7069eqrdv 2822 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 “ {(𝑀𝑤)}) = (𝑆 “ {(𝑁𝑤)}))
71 relinxp 5674 . . . . . . . . . . . . . . . . . . 19 Rel (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))
72 relinxp 5674 . . . . . . . . . . . . . . . . . . 19 Rel (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))
73 vex 3483 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 ∈ V
7473eliniseg 5945 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀𝑤) ∈ V → (𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑧𝑅(𝑀𝑤)))
7564, 74anbi12d 633 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀𝑤) ∈ V → ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ↔ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤))))
7662, 75ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ↔ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤)))
7756simprd 499 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → (𝑧𝑅(𝑀𝑤) → (𝑦𝑅𝑧𝑦𝑆𝑧)))
7877impr 458 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤))) → (𝑦𝑅𝑧𝑦𝑆𝑧))
7976, 78sylan2b 596 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}))) → (𝑦𝑅𝑧𝑦𝑆𝑧))
8079pm5.32da 582 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧)))
81 df-br 5053 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
82 brinxp2 5616 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧))
8381, 82bitr3i 280 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧))
84 df-br 5053 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
85 brinxp2 5616 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧))
8684, 85bitr3i 280 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧))
8780, 83, 863bitr4g 317 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))))
8871, 72, 87eqrelrdv 5652 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
8970sqxpeqd 5574 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) = ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))
9089ineq2d 4174 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)}))))
9188, 90eqtrd 2859 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)}))))
9270, 91oveq12d 7167 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))))
932ffvelrni 6841 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ dom 𝑀 → (𝑀𝑤) ∈ 𝑋)
9493adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) ∈ 𝑋)
9594adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) ∈ 𝑋)
9642, 43, 48fpwwe2lem3 10053 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑀𝑤) ∈ 𝑋) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = (𝑀𝑤))
9745, 95, 96syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = (𝑀𝑤))
986ffvelrni 6841 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ dom 𝑁 → (𝑁𝑤) ∈ 𝑌)
9953, 98syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → (𝑁𝑤) ∈ 𝑌)
10099adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑁𝑤) ∈ 𝑌)
10142, 43, 50fpwwe2lem3 10053 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑁𝑤) ∈ 𝑌) → ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))) = (𝑁𝑤))
10245, 100, 101syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))) = (𝑁𝑤))
10392, 97, 1023eqtr3d 2867 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) = (𝑁𝑤))
104103ex 416 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) → (𝑀𝑤) = (𝑁𝑤)))
10541, 104sylbird 263 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦) → (𝑀𝑤) = (𝑁𝑤)))
10628, 105syld 47 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑤) = (𝑁𝑤)))
107106ex 416 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ dom 𝑀 → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑤) = (𝑁𝑤))))
108107com23 86 . . . . . . . . . 10 (𝜑 → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
109108a2i 14 . . . . . . . . 9 ((𝜑 → ∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
11021, 109sylbi 220 . . . . . . . 8 (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
111110a1i 11 . . . . . . 7 (𝑤 ∈ On → (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)))))
11220, 111tfis2 7565 . . . . . 6 (𝑤 ∈ On → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
113112com3l 89 . . . . 5 (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑤 ∈ On → (𝑀𝑤) = (𝑁𝑤))))
11414, 113mpdi 45 . . . 4 (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)))
115114imp 410 . . 3 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) = (𝑁𝑤))
116 fvres 6680 . . . 4 (𝑤 ∈ dom 𝑀 → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁𝑤))
117116adantl 485 . . 3 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁𝑤))
118115, 117eqtr4d 2862 . 2 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) = ((𝑁 ↾ dom 𝑀)‘𝑤))
1194, 11, 118eqfnfvd 6796 1 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∀wral 3133  Vcvv 3480  [wsbc 3758   ∩ cin 3918   ⊆ wss 3919  {csn 4550  ⟨cop 4556   class class class wbr 5052  {copab 5114   We wwe 5500   × cxp 5540  ◡ccnv 5541  dom cdm 5542   ↾ cres 5544   “ cima 5545  Ord word 6177  Oncon0 6178   Fn wfn 6338  ⟶wf 6339  ‘cfv 6343  (class class class)co 7149  OrdIsocoi 8970 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-wrecs 7943  df-recs 8004  df-oi 8971 This theorem is referenced by:  fpwwe2lem9  10058
 Copyright terms: Public domain W3C validator