Metamath Proof Explorer

Theorem fpwwe2lem8

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)

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

Proof

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