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

Theorem fpwwe2lem8 9661
 Description: Lemma for fpwwe2 9667. Show by induction that the two isometries 𝑀 and 𝑁 agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.)
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 8591 . . 3 𝑀:dom 𝑀𝑋
3 ffn 6185 . . 3 (𝑀:dom 𝑀𝑋𝑀 Fn dom 𝑀)
42, 3mp1i 13 . 2 (𝜑𝑀 Fn dom 𝑀)
5 fpwwe2lem9.n . . . . 5 𝑁 = OrdIso(𝑆, 𝑌)
65oif 8591 . . . 4 𝑁:dom 𝑁𝑌
7 ffn 6185 . . . 4 (𝑁:dom 𝑁𝑌𝑁 Fn dom 𝑁)
86, 7mp1i 13 . . 3 (𝜑𝑁 Fn dom 𝑁)
9 fpwwe2lem9.s . . 3 (𝜑 → dom 𝑀 ⊆ dom 𝑁)
10 fnssres 6144 . . 3 ((𝑁 Fn dom 𝑁 ∧ dom 𝑀 ⊆ dom 𝑁) → (𝑁 ↾ dom 𝑀) Fn dom 𝑀)
118, 9, 10syl2anc 573 . 2 (𝜑 → (𝑁 ↾ dom 𝑀) Fn dom 𝑀)
121oicl 8590 . . . . . 6 Ord dom 𝑀
13 ordelon 5890 . . . . . 6 ((Ord dom 𝑀𝑤 ∈ dom 𝑀) → 𝑤 ∈ On)
1412, 13mpan 670 . . . . 5 (𝑤 ∈ dom 𝑀𝑤 ∈ On)
15 eleq1w 2833 . . . . . . . . 9 (𝑤 = 𝑦 → (𝑤 ∈ dom 𝑀𝑦 ∈ dom 𝑀))
16 fveq2 6332 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑀𝑤) = (𝑀𝑦))
17 fveq2 6332 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑁𝑤) = (𝑁𝑦))
1816, 17eqeq12d 2786 . . . . . . . . 9 (𝑤 = 𝑦 → ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑀𝑦) = (𝑁𝑦)))
1915, 18imbi12d 333 . . . . . . . 8 (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)) ↔ (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))))
2019imbi2d 329 . . . . . . 7 (𝑤 = 𝑦 → ((𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))) ↔ (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)))))
21 r19.21v 3109 . . . . . . . . 9 (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) ↔ (𝜑 → ∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))))
2212a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord dom 𝑀)
23 ordelss 5882 . . . . . . . . . . . . . . . . 17 ((Ord dom 𝑀𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀)
2422, 23sylan 569 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑀)
2524sselda 3752 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ dom 𝑀) ∧ 𝑦𝑤) → 𝑦 ∈ dom 𝑀)
26 pm2.27 42 . . . . . . . . . . . . . . 15 (𝑦 ∈ dom 𝑀 → ((𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑦) = (𝑁𝑦)))
2725, 26syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑤 ∈ dom 𝑀) ∧ 𝑦𝑤) → ((𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑦) = (𝑁𝑦)))
2827ralimdva 3111 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦)))
294adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ dom 𝑀) → 𝑀 Fn dom 𝑀)
30 fnssres 6144 . . . . . . . . . . . . . . . . 17 ((𝑀 Fn dom 𝑀𝑤 ⊆ dom 𝑀) → (𝑀𝑤) Fn 𝑤)
3129, 24, 30syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) Fn 𝑤)
328adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ dom 𝑀) → 𝑁 Fn dom 𝑁)
339adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → dom 𝑀 ⊆ dom 𝑁)
3424, 33sstrd 3762 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ⊆ dom 𝑁)
35 fnssres 6144 . . . . . . . . . . . . . . . . 17 ((𝑁 Fn dom 𝑁𝑤 ⊆ dom 𝑁) → (𝑁𝑤) Fn 𝑤)
3632, 34, 35syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ dom 𝑀) → (𝑁𝑤) Fn 𝑤)
37 eqfnfv 6454 . . . . . . . . . . . . . . . 16 (((𝑀𝑤) Fn 𝑤 ∧ (𝑁𝑤) Fn 𝑤) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦)))
3831, 36, 37syl2anc 573 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦)))
39 fvres 6348 . . . . . . . . . . . . . . . . 17 (𝑦𝑤 → ((𝑀𝑤)‘𝑦) = (𝑀𝑦))
40 fvres 6348 . . . . . . . . . . . . . . . . 17 (𝑦𝑤 → ((𝑁𝑤)‘𝑦) = (𝑁𝑦))
4139, 40eqeq12d 2786 . . . . . . . . . . . . . . . 16 (𝑦𝑤 → (((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦) ↔ (𝑀𝑦) = (𝑁𝑦)))
4241ralbiia 3128 . . . . . . . . . . . . . . 15 (∀𝑦𝑤 ((𝑀𝑤)‘𝑦) = ((𝑁𝑤)‘𝑦) ↔ ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦))
4338, 42syl6bb 276 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) ↔ ∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦)))
44 fpwwe2.1 . . . . . . . . . . . . . . . . . . . . . 22 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
45 fpwwe2.2 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ V)
4645ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝐴 ∈ V)
47 simpll 750 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝜑)
48 fpwwe2.3 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
4947, 48sylan 569 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
50 fpwwe2lem9.x . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑋𝑊𝑅)
5150ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑋𝑊𝑅)
52 fpwwe2lem9.y . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑌𝑊𝑆)
5352ad2antrr 705 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑌𝑊𝑆)
54 simplr 752 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑤 ∈ dom 𝑀)
559sselda 3752 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ dom 𝑀) → 𝑤 ∈ dom 𝑁)
5655adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → 𝑤 ∈ dom 𝑁)
57 simpr 471 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) = (𝑁𝑤))
5844, 46, 49, 51, 53, 1, 5, 54, 56, 57fpwwe2lem7 9660 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → (𝑦𝑆(𝑁𝑤) ∧ (𝑧𝑅(𝑀𝑤) → (𝑦𝑅𝑧𝑦𝑆𝑧))))
5958simpld 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → 𝑦𝑆(𝑁𝑤))
6057eqcomd 2777 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑁𝑤) = (𝑀𝑤))
6144, 46, 49, 53, 51, 5, 1, 56, 54, 60fpwwe2lem7 9660 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑆(𝑁𝑤)) → (𝑦𝑅(𝑀𝑤) ∧ (𝑧𝑆(𝑁𝑤) → (𝑦𝑆𝑧𝑦𝑅𝑧))))
6261simpld 482 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑆(𝑁𝑤)) → 𝑦𝑅(𝑀𝑤))
6359, 62impbida 802 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑦𝑅(𝑀𝑤) ↔ 𝑦𝑆(𝑁𝑤)))
64 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑀𝑤) ∈ V
65 vex 3354 . . . . . . . . . . . . . . . . . . . . 21 𝑦 ∈ V
6665eliniseg 5635 . . . . . . . . . . . . . . . . . . . 20 ((𝑀𝑤) ∈ V → (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦𝑅(𝑀𝑤)))
6764, 66ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦𝑅(𝑀𝑤))
68 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑁𝑤) ∈ V
6965eliniseg 5635 . . . . . . . . . . . . . . . . . . . 20 ((𝑁𝑤) ∈ V → (𝑦 ∈ (𝑆 “ {(𝑁𝑤)}) ↔ 𝑦𝑆(𝑁𝑤)))
7068, 69ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (𝑆 “ {(𝑁𝑤)}) ↔ 𝑦𝑆(𝑁𝑤))
7163, 67, 703bitr4g 303 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑦 ∈ (𝑆 “ {(𝑁𝑤)})))
7271eqrdv 2769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 “ {(𝑀𝑤)}) = (𝑆 “ {(𝑁𝑤)}))
73 inss2 3982 . . . . . . . . . . . . . . . . . . . 20 (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ⊆ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))
74 relxp 5266 . . . . . . . . . . . . . . . . . . . 20 Rel ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))
75 relss 5346 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ⊆ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) → (Rel ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) → Rel (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))))
7673, 74, 75mp2 9 . . . . . . . . . . . . . . . . . . 19 Rel (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))
77 inss2 3982 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ⊆ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))
78 relss 5346 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ⊆ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) → (Rel ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) → Rel (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))))
7977, 74, 78mp2 9 . . . . . . . . . . . . . . . . . . 19 Rel (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))
80 vex 3354 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑧 ∈ V
8180eliniseg 5635 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀𝑤) ∈ V → (𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ↔ 𝑧𝑅(𝑀𝑤)))
8266, 81anbi12d 616 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀𝑤) ∈ V → ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ↔ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤))))
8364, 82ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ↔ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤)))
8458simprd 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ 𝑦𝑅(𝑀𝑤)) → (𝑧𝑅(𝑀𝑤) → (𝑦𝑅𝑧𝑦𝑆𝑧)))
8584impr 442 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑦𝑅(𝑀𝑤) ∧ 𝑧𝑅(𝑀𝑤))) → (𝑦𝑅𝑧𝑦𝑆𝑧))
8683, 85sylan2b 581 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) ∧ (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}))) → (𝑦𝑅𝑧𝑦𝑆𝑧))
8786pm5.32da 568 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧)))
88 brinxp2 5320 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑦𝑅𝑧))
89 df-br 4787 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
90 df-3an 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑦𝑅𝑧) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧))
9188, 89, 903bitr3i 290 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑅𝑧))
92 brinxp2 5320 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ (𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑦𝑆𝑧))
93 df-br 4787 . . . . . . . . . . . . . . . . . . . . 21 (𝑦(𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
94 df-3an 1073 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑦𝑆𝑧) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧))
9592, 93, 943bitr3i 290 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ((𝑦 ∈ (𝑅 “ {(𝑀𝑤)}) ∧ 𝑧 ∈ (𝑅 “ {(𝑀𝑤)})) ∧ 𝑦𝑆𝑧))
9687, 91, 953bitr4g 303 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (⟨𝑦, 𝑧⟩ ∈ (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) ↔ ⟨𝑦, 𝑧⟩ ∈ (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))))
9776, 79, 96eqrelrdv 5356 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))))
9872sqxpeqd 5281 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})) = ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))
9998ineq2d 3965 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑆 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)}))))
10097, 99eqtrd 2805 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)}))) = (𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)}))))
10172, 100oveq12d 6811 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))))
1022ffvelrni 6501 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ dom 𝑀 → (𝑀𝑤) ∈ 𝑋)
103102adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) ∈ 𝑋)
104103adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) ∈ 𝑋)
10544, 45, 50fpwwe2lem3 9657 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑀𝑤) ∈ 𝑋) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = (𝑀𝑤))
10647, 104, 105syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑅 “ {(𝑀𝑤)})𝐹(𝑅 ∩ ((𝑅 “ {(𝑀𝑤)}) × (𝑅 “ {(𝑀𝑤)})))) = (𝑀𝑤))
1076ffvelrni 6501 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ dom 𝑁 → (𝑁𝑤) ∈ 𝑌)
10855, 107syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤 ∈ dom 𝑀) → (𝑁𝑤) ∈ 𝑌)
109108adantr 466 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑁𝑤) ∈ 𝑌)
11044, 45, 52fpwwe2lem3 9657 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑁𝑤) ∈ 𝑌) → ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))) = (𝑁𝑤))
11147, 109, 110syl2anc 573 . . . . . . . . . . . . . . . 16 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → ((𝑆 “ {(𝑁𝑤)})𝐹(𝑆 ∩ ((𝑆 “ {(𝑁𝑤)}) × (𝑆 “ {(𝑁𝑤)})))) = (𝑁𝑤))
112101, 106, 1113eqtr3d 2813 . . . . . . . . . . . . . . 15 (((𝜑𝑤 ∈ dom 𝑀) ∧ (𝑀𝑤) = (𝑁𝑤)) → (𝑀𝑤) = (𝑁𝑤))
113112ex 397 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑀𝑤) = (𝑁𝑤) → (𝑀𝑤) = (𝑁𝑤)))
11443, 113sylbird 250 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑀𝑦) = (𝑁𝑦) → (𝑀𝑤) = (𝑁𝑤)))
11528, 114syld 47 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ dom 𝑀) → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑤) = (𝑁𝑤)))
116115ex 397 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ dom 𝑀 → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑀𝑤) = (𝑁𝑤))))
117116com23 86 . . . . . . . . . 10 (𝜑 → (∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦)) → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
118117a2i 14 . . . . . . . . 9 ((𝜑 → ∀𝑦𝑤 (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
11921, 118sylbi 207 . . . . . . . 8 (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
120119a1i 11 . . . . . . 7 (𝑤 ∈ On → (∀𝑦𝑤 (𝜑 → (𝑦 ∈ dom 𝑀 → (𝑀𝑦) = (𝑁𝑦))) → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)))))
12120, 120tfis2 7203 . . . . . 6 (𝑤 ∈ On → (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤))))
122121com3l 89 . . . . 5 (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑤 ∈ On → (𝑀𝑤) = (𝑁𝑤))))
12314, 122mpdi 45 . . . 4 (𝜑 → (𝑤 ∈ dom 𝑀 → (𝑀𝑤) = (𝑁𝑤)))
124123imp 393 . . 3 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) = (𝑁𝑤))
125 fvres 6348 . . . 4 (𝑤 ∈ dom 𝑀 → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁𝑤))
126125adantl 467 . . 3 ((𝜑𝑤 ∈ dom 𝑀) → ((𝑁 ↾ dom 𝑀)‘𝑤) = (𝑁𝑤))
127124, 126eqtr4d 2808 . 2 ((𝜑𝑤 ∈ dom 𝑀) → (𝑀𝑤) = ((𝑁 ↾ dom 𝑀)‘𝑤))
1284, 11, 127eqfnfvd 6457 1 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145  ∀wral 3061  Vcvv 3351  [wsbc 3587   ∩ cin 3722   ⊆ wss 3723  {csn 4316  ⟨cop 4322   class class class wbr 4786  {copab 4846   We wwe 5207   × cxp 5247  ◡ccnv 5248  dom cdm 5249   ↾ cres 5251   “ cima 5252  Rel wrel 5254  Ord word 5865  Oncon0 5866   Fn wfn 6026  ⟶wf 6027  ‘cfv 6031  (class class class)co 6793  OrdIsocoi 8570 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-wrecs 7559  df-recs 7621  df-oi 8571 This theorem is referenced by:  fpwwe2lem9  9662
 Copyright terms: Public domain W3C validator