Metamath Proof Explorer

Theorem fpwwe2lem7

Description: Lemma for fpwwe2 . Show by induction that the two isometries M and N agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
fpwwe2lem8.x ⊢ ( 𝜑 → 𝑋 𝑊 𝑅 )
fpwwe2lem8.y ⊢ ( 𝜑 → 𝑌 𝑊 𝑆 )
fpwwe2lem8.m ⊢ 𝑀 = OrdIso ( 𝑅 , 𝑋 )
fpwwe2lem8.n ⊢ 𝑁 = OrdIso ( 𝑆 , 𝑌 )
fpwwe2lem8.s ⊢ ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
Assertion fpwwe2lem7 ( 𝜑 → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 fpwwe2lem8.x ⊢ ( 𝜑 → 𝑋 𝑊 𝑅 )
5 fpwwe2lem8.y ⊢ ( 𝜑 → 𝑌 𝑊 𝑆 )
6 fpwwe2lem8.m ⊢ 𝑀 = OrdIso ( 𝑅 , 𝑋 )
7 fpwwe2lem8.n ⊢ 𝑁 = OrdIso ( 𝑆 , 𝑌 )
8 fpwwe2lem8.s ⊢ ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
9 6 oif ⊢ 𝑀 : dom 𝑀 ⟶ 𝑋
10 ffn ⊢ ( 𝑀 : dom 𝑀 ⟶ 𝑋 → 𝑀 Fn dom 𝑀 )
11 9 10 mp1i ⊢ ( 𝜑 → 𝑀 Fn dom 𝑀 )
12 7 oif ⊢ 𝑁 : dom 𝑁 ⟶ 𝑌
13 ffn ⊢ ( 𝑁 : dom 𝑁 ⟶ 𝑌 → 𝑁 Fn dom 𝑁 )
14 12 13 mp1i ⊢ ( 𝜑 → 𝑁 Fn dom 𝑁 )
15 14 8 fnssresd ⊢ ( 𝜑 → ( 𝑁 ↾ dom 𝑀 ) Fn dom 𝑀 )
16 6 oicl ⊢ Ord dom 𝑀
17 ordelon ⊢ ( ( Ord dom 𝑀 ∧ 𝑤 ∈ dom 𝑀 ) → 𝑤 ∈ On )
18 16 17 mpan ⊢ ( 𝑤 ∈ dom 𝑀 → 𝑤 ∈ On )
19 eleq1w ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ dom 𝑀 ↔ 𝑦 ∈ dom 𝑀 ) )
20 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑀 ‘ 𝑤 ) = ( 𝑀 ‘ 𝑦 ) )
21 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑁 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑦 ) )
22 20 21 eqeq12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ↔ ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
23 19 22 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ↔ ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) )
24 23 imbi2d ⊢ ( 𝑤 = 𝑦 → ( ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) ) )
25 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝜑 → ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( 𝜑 → ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) )
26 16 a1i ⊢ ( 𝜑 → Ord dom 𝑀 )
27 ordelss ⊢ ( ( Ord dom 𝑀 ∧ 𝑤 ∈ dom 𝑀 ) → 𝑤 ⊆ dom 𝑀 )
28 26 27 sylan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → 𝑤 ⊆ dom 𝑀 )
29 28 sselda ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ∈ dom 𝑀 )
30 pm2.27 ⊢ ( 𝑦 ∈ dom 𝑀 → ( ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
31 29 30 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ 𝑦 ∈ 𝑤 ) → ( ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
32 31 ralimdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ 𝑤 ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
33 fnssres ⊢ ( ( 𝑀 Fn dom 𝑀 ∧ 𝑤 ⊆ dom 𝑀 ) → ( 𝑀 ↾ 𝑤 ) Fn 𝑤 )
34 11 28 33 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑀 ↾ 𝑤 ) Fn 𝑤 )
35 8 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → dom 𝑀 ⊆ dom 𝑁 )
36 28 35 sstrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → 𝑤 ⊆ dom 𝑁 )
37 fnssres ⊢ ( ( 𝑁 Fn dom 𝑁 ∧ 𝑤 ⊆ dom 𝑁 ) → ( 𝑁 ↾ 𝑤 ) Fn 𝑤 )
38 14 36 37 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑁 ↾ 𝑤 ) Fn 𝑤 )
39 eqfnfv ⊢ ( ( ( 𝑀 ↾ 𝑤 ) Fn 𝑤 ∧ ( 𝑁 ↾ 𝑤 ) Fn 𝑤 ) → ( ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝑤 ( ( 𝑀 ↾ 𝑤 ) ‘ 𝑦 ) = ( ( 𝑁 ↾ 𝑤 ) ‘ 𝑦 ) ) )
40 34 38 39 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝑤 ( ( 𝑀 ↾ 𝑤 ) ‘ 𝑦 ) = ( ( 𝑁 ↾ 𝑤 ) ‘ 𝑦 ) ) )
41 fvres ⊢ ( 𝑦 ∈ 𝑤 → ( ( 𝑀 ↾ 𝑤 ) ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) )
42 fvres ⊢ ( 𝑦 ∈ 𝑤 → ( ( 𝑁 ↾ 𝑤 ) ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
43 41 42 eqeq12d ⊢ ( 𝑦 ∈ 𝑤 → ( ( ( 𝑀 ↾ 𝑤 ) ‘ 𝑦 ) = ( ( 𝑁 ↾ 𝑤 ) ‘ 𝑦 ) ↔ ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
44 43 ralbiia ⊢ ( ∀ 𝑦 ∈ 𝑤 ( ( 𝑀 ↾ 𝑤 ) ‘ 𝑦 ) = ( ( 𝑁 ↾ 𝑤 ) ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
45 40 44 bitrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝑤 ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) )
46 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝐴 ∈ 𝑉 )
47 simpll ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝜑 )
48 47 3 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
49 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝑋 𝑊 𝑅 )
50 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝑌 𝑊 𝑆 )
51 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝑤 ∈ dom 𝑀 )
52 8 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → 𝑤 ∈ dom 𝑁 )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → 𝑤 ∈ dom 𝑁 )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) )
55 1 46 48 49 50 6 7 51 53 54 fpwwe2lem6 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ) → ( 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) ∧ ( 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) ) ) )
56 55 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ) → 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) )
57 54 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑁 ↾ 𝑤 ) = ( 𝑀 ↾ 𝑤 ) )
58 1 46 48 50 49 7 6 53 51 57 fpwwe2lem6 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) ) → ( 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ∧ ( 𝑧 𝑆 ( 𝑁 ‘ 𝑤 ) → ( 𝑦 𝑆 𝑧 ↔ 𝑦 𝑅 𝑧 ) ) ) )
59 58 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) ) → 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) )
60 56 59 impbida ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ↔ 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) ) )
61 fvex ⊢ ( 𝑀 ‘ 𝑤 ) ∈ V
62 vex ⊢ 𝑦 ∈ V
63 62 eliniseg ⊢ ( ( 𝑀 ‘ 𝑤 ) ∈ V → ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ↔ 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ) )
64 61 63 ax-mp ⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ↔ 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) )
65 fvex ⊢ ( 𝑁 ‘ 𝑤 ) ∈ V
66 62 eliniseg ⊢ ( ( 𝑁 ‘ 𝑤 ) ∈ V → ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ↔ 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) ) )
67 65 66 ax-mp ⊢ ( 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ↔ 𝑦 𝑆 ( 𝑁 ‘ 𝑤 ) )
68 60 64 67 3bitr4g ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ↔ 𝑦 ∈ ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) )
69 68 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) = ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) )
70 relinxp ⊢ Rel ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) )
71 relinxp ⊢ Rel ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) )
72 vex ⊢ 𝑧 ∈ V
73 72 eliniseg ⊢ ( ( 𝑀 ‘ 𝑤 ) ∈ V → ( 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ↔ 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) ) )
74 63 73 anbi12d ⊢ ( ( 𝑀 ‘ 𝑤 ) ∈ V → ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ↔ ( 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ∧ 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) ) ) )
75 61 74 ax-mp ⊢ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ↔ ( 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ∧ 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) ) )
76 55 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ) → ( 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) ) )
77 76 impr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ ( 𝑦 𝑅 ( 𝑀 ‘ 𝑤 ) ∧ 𝑧 𝑅 ( 𝑀 ‘ 𝑤 ) ) ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) )
78 75 77 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) ∧ ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) )
79 78 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑅 𝑧 ) ↔ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑆 𝑧 ) ) )
80 df-br ⊢ ( 𝑦 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) )
81 brinxp2 ⊢ ( 𝑦 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) 𝑧 ↔ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑅 𝑧 ) )
82 80 81 bitr3i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ↔ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑅 𝑧 ) )
83 df-br ⊢ ( 𝑦 ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) )
84 brinxp2 ⊢ ( 𝑦 ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) 𝑧 ↔ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑆 𝑧 ) )
85 83 84 bitr3i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ↔ ( ( 𝑦 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ∧ 𝑧 ∈ ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ∧ 𝑦 𝑆 𝑧 ) )
86 79 82 85 3bitr4g ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ) )
87 70 71 86 eqrelrdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) = ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) )
88 69 sqxpeqd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) = ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) )
89 88 ineq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑆 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) = ( 𝑆 ∩ ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) ) )
90 87 89 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) = ( 𝑆 ∩ ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) ) )
91 69 90 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ) = ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) 𝐹 ( 𝑆 ∩ ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) ) ) )
92 9 ffvelrni ⊢ ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) ∈ 𝑋 )
93 92 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑀 ‘ 𝑤 ) ∈ 𝑋 )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑀 ‘ 𝑤 ) ∈ 𝑋 )
95 1 2 4 fpwwe2lem3 ⊢ ( ( 𝜑 ∧ ( 𝑀 ‘ 𝑤 ) ∈ 𝑋 ) → ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ) = ( 𝑀 ‘ 𝑤 ) )
96 47 94 95 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) × ( ◡ 𝑅 “ { ( 𝑀 ‘ 𝑤 ) } ) ) ) ) = ( 𝑀 ‘ 𝑤 ) )
97 12 ffvelrni ⊢ ( 𝑤 ∈ dom 𝑁 → ( 𝑁 ‘ 𝑤 ) ∈ 𝑌 )
98 52 97 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑁 ‘ 𝑤 ) ∈ 𝑌 )
99 98 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑁 ‘ 𝑤 ) ∈ 𝑌 )
100 1 2 5 fpwwe2lem3 ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ 𝑤 ) ∈ 𝑌 ) → ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) 𝐹 ( 𝑆 ∩ ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) ) ) = ( 𝑁 ‘ 𝑤 ) )
101 47 99 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) 𝐹 ( 𝑆 ∩ ( ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) × ( ◡ 𝑆 “ { ( 𝑁 ‘ 𝑤 ) } ) ) ) ) = ( 𝑁 ‘ 𝑤 ) )
102 91 96 101 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) ∧ ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) )
103 102 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ( 𝑀 ↾ 𝑤 ) = ( 𝑁 ↾ 𝑤 ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) )
104 45 103 sylbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ∀ 𝑦 ∈ 𝑤 ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) )
105 32 104 syld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) )
106 105 ex ⊢ ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
107 106 com23 ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
108 107 a2i ⊢ ( ( 𝜑 → ∀ 𝑦 ∈ 𝑤 ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
109 25 108 sylbi ⊢ ( ∀ 𝑦 ∈ 𝑤 ( 𝜑 → ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
110 109 a1i ⊢ ( 𝑤 ∈ On → ( ∀ 𝑦 ∈ 𝑤 ( 𝜑 → ( 𝑦 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) ) ) → ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) ) )
111 24 110 tfis2 ⊢ ( 𝑤 ∈ On → ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
112 111 com3l ⊢ ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑤 ∈ On → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) ) )
113 18 112 mpdi ⊢ ( 𝜑 → ( 𝑤 ∈ dom 𝑀 → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) ) )
114 113 imp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑀 ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) )
115 fvres ⊢ ( 𝑤 ∈ dom 𝑀 → ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) )
116 115 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑤 ) = ( 𝑁 ‘ 𝑤 ) )
117 114 116 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ dom 𝑀 ) → ( 𝑀 ‘ 𝑤 ) = ( ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑤 ) )
118 11 15 117 eqfnfvd ⊢ ( 𝜑 → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )