This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fpwwe2lem6

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (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 ( 𝑆 , 𝑌 )
fpwwe2lem5.1 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
fpwwe2lem5.2 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑁 )
fpwwe2lem5.3 ⊢ ( 𝜑 → ( 𝑀 ↾ 𝐵 ) = ( 𝑁 ↾ 𝐵 ) )
Assertion fpwwe2lem6 ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 𝑆 ( 𝑁 ‘ 𝐵 ) ∧ ( 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) → ( 𝐶 𝑅 𝐷 ↔ 𝐶 𝑆 𝐷 ) ) ) )

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 fpwwe2lem5.1 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
9 fpwwe2lem5.2 ⊢ ( 𝜑 → 𝐵 ∈ dom 𝑁 )
10 fpwwe2lem5.3 ⊢ ( 𝜑 → ( 𝑀 ↾ 𝐵 ) = ( 𝑁 ↾ 𝐵 ) )
11 1 relopabiv ⊢ Rel 𝑊
12 11 brrelex1i ⊢ ( 𝑌 𝑊 𝑆 → 𝑌 ∈ V )
13 5 12 syl ⊢ ( 𝜑 → 𝑌 ∈ V )
14 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑌 𝑊 𝑆 ↔ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
15 5 14 mpbid ⊢ ( 𝜑 → ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
16 15 simprld ⊢ ( 𝜑 → 𝑆 We 𝑌 )
17 7 oiiso ⊢ ( ( 𝑌 ∈ V ∧ 𝑆 We 𝑌 ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
18 13 16 17 syl2anc ⊢ ( 𝜑 → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
20 isof1o ⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 )
21 19 20 syl ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 )
22 1 2 3 4 5 6 7 8 9 10 fpwwe2lem5 ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) ) )
23 22 simp2d ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ 𝑌 )
24 f1ocnvfv2 ⊢ ( ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 ∧ 𝐶 ∈ 𝑌 ) → ( 𝑁 ‘ ( ◡ 𝑁 ‘ 𝐶 ) ) = 𝐶 )
25 21 23 24 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑁 ‘ ( ◡ 𝑁 ‘ 𝐶 ) ) = 𝐶 )
26 22 simp3d ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) )
27 11 brrelex1i ⊢ ( 𝑋 𝑊 𝑅 → 𝑋 ∈ V )
28 4 27 syl ⊢ ( 𝜑 → 𝑋 ∈ V )
29 1 2 fpwwe2lem2 ⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
30 4 29 mpbid ⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
31 30 simprld ⊢ ( 𝜑 → 𝑅 We 𝑋 )
32 6 oiiso ⊢ ( ( 𝑋 ∈ V ∧ 𝑅 We 𝑋 ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
33 28 31 32 syl2anc ⊢ ( 𝜑 → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
35 isof1o ⊢ ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 )
37 22 simp1d ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ 𝑋 )
38 f1ocnvfv2 ⊢ ( ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) = 𝐶 )
39 36 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) = 𝐶 )
40 simpr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) )
41 39 40 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) )
42 f1ocnv ⊢ ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 → ◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 )
43 f1of ⊢ ( ◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 → ◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
44 36 42 43 3syl ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
45 44 37 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) ∈ dom 𝑀 )
46 8 adantr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ∈ dom 𝑀 )
47 isorel ⊢ ( ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) ∧ ( ( ◡ 𝑀 ‘ 𝐶 ) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀 ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) ) )
48 34 45 46 47 syl12anc ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) ) )
49 41 48 mpbird ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 )
50 26 49 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑁 ‘ 𝐶 ) E 𝐵 )
51 f1ocnv ⊢ ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 → ◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 )
52 f1of ⊢ ( ◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 → ◡ 𝑁 : 𝑌 ⟶ dom 𝑁 )
53 21 51 52 3syl ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ 𝑁 : 𝑌 ⟶ dom 𝑁 )
54 53 23 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑁 ‘ 𝐶 ) ∈ dom 𝑁 )
55 9 adantr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ∈ dom 𝑁 )
56 isorel ⊢ ( ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) ∧ ( ( ◡ 𝑁 ‘ 𝐶 ) ∈ dom 𝑁 ∧ 𝐵 ∈ dom 𝑁 ) ) → ( ( ◡ 𝑁 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑁 ‘ ( ◡ 𝑁 ‘ 𝐶 ) ) 𝑆 ( 𝑁 ‘ 𝐵 ) ) )
57 19 54 55 56 syl12anc ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑁 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑁 ‘ ( ◡ 𝑁 ‘ 𝐶 ) ) 𝑆 ( 𝑁 ‘ 𝐵 ) ) )
58 50 57 mpbid ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑁 ‘ ( ◡ 𝑁 ‘ 𝐶 ) ) 𝑆 ( 𝑁 ‘ 𝐵 ) )
59 25 58 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 𝑆 ( 𝑁 ‘ 𝐵 ) )
60 26 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) )
61 1 2 3 4 5 6 7 8 9 10 fpwwe2lem5 ⊢ ( ( 𝜑 ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐷 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ∧ ( ◡ 𝑀 ‘ 𝐷 ) = ( ◡ 𝑁 ‘ 𝐷 ) ) )
62 61 simp3d ⊢ ( ( 𝜑 ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐷 ) = ( ◡ 𝑁 ‘ 𝐷 ) )
63 62 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( ◡ 𝑀 ‘ 𝐷 ) = ( ◡ 𝑁 ‘ 𝐷 ) )
64 60 63 breq12d ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E ( ◡ 𝑀 ‘ 𝐷 ) ↔ ( ◡ 𝑁 ‘ 𝐶 ) E ( ◡ 𝑁 ‘ 𝐷 ) ) )
65 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
66 isocnv ⊢ ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → ◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
67 65 66 syl ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
68 37 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝐶 ∈ 𝑋 )
69 30 simplrd ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑋 × 𝑋 ) )
70 69 ssbrd ⊢ ( 𝜑 → ( 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) → 𝐷 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) ) )
71 70 imp ⊢ ( ( 𝜑 ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) )
72 brxp ⊢ ( 𝐷 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) ↔ ( 𝐷 ∈ 𝑋 ∧ ( 𝑀 ‘ 𝐵 ) ∈ 𝑋 ) )
73 72 simplbi ⊢ ( 𝐷 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) → 𝐷 ∈ 𝑋 )
74 71 73 syl ⊢ ( ( 𝜑 ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ∈ 𝑋 )
75 74 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝐷 ∈ 𝑋 )
76 isorel ⊢ ( ( ◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( 𝐶 𝑅 𝐷 ↔ ( ◡ 𝑀 ‘ 𝐶 ) E ( ◡ 𝑀 ‘ 𝐷 ) ) )
77 67 68 75 76 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐶 𝑅 𝐷 ↔ ( ◡ 𝑀 ‘ 𝐶 ) E ( ◡ 𝑀 ‘ 𝐷 ) ) )
78 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
79 isocnv ⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
80 78 79 syl ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
81 23 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝐶 ∈ 𝑌 )
82 61 simp2d ⊢ ( ( 𝜑 ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐷 ∈ 𝑌 )
83 82 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → 𝐷 ∈ 𝑌 )
84 isorel ⊢ ( ( ◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) ∧ ( 𝐶 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌 ) ) → ( 𝐶 𝑆 𝐷 ↔ ( ◡ 𝑁 ‘ 𝐶 ) E ( ◡ 𝑁 ‘ 𝐷 ) ) )
85 80 81 83 84 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐶 𝑆 𝐷 ↔ ( ◡ 𝑁 ‘ 𝐶 ) E ( ◡ 𝑁 ‘ 𝐷 ) ) )
86 64 77 85 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ∧ 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) ) ) → ( 𝐶 𝑅 𝐷 ↔ 𝐶 𝑆 𝐷 ) )
87 86 expr ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) → ( 𝐶 𝑅 𝐷 ↔ 𝐶 𝑆 𝐷 ) ) )
88 59 87 jca ⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 𝑆 ( 𝑁 ‘ 𝐵 ) ∧ ( 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) → ( 𝐶 𝑅 𝐷 ↔ 𝐶 𝑆 𝐷 ) ) ) )