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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) ∈ 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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑁 ‘ 𝐶 ) ∈ 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	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 𝑆 ( 𝑁 ‘ 𝐵 ) ∧ ( 𝐷 𝑅 ( 𝑀 ‘ 𝐵 ) → ( 𝐶 𝑅 𝐷 ↔ 𝐶 𝑆 𝐷 ) ) ) )