erlval

Description: Value of the ring localization equivalence relation. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	rlocval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rlocval.2	⊢ 0 = ( 0_g ‘ 𝑅 )
	rlocval.3	⊢ · = ( ._r ‘ 𝑅 )
	rlocval.4	⊢ − = ( -_g ‘ 𝑅 )
	erlval.w	⊢ 𝑊 = ( 𝐵 × 𝑆 )
	erlval.q	⊢ ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) }
	erlval.20	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion	erlval	⊢ ( 𝜑 → ( 𝑅 ~_RL 𝑆 ) = ∼ )

Proof

Step	Hyp	Ref	Expression
1		rlocval.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rlocval.2	⊢ 0 = ( 0_g ‘ 𝑅 )
3		rlocval.3	⊢ · = ( ._r ‘ 𝑅 )
4		rlocval.4	⊢ − = ( -_g ‘ 𝑅 )
5		erlval.w	⊢ 𝑊 = ( 𝐵 × 𝑆 )
6		erlval.q	⊢ ∼ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) }
7		erlval.20	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
9	1	fvexi	⊢ 𝐵 ∈ V
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝐵 ∈ V )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑆 ⊆ 𝐵 )
12	10 11	ssexd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑆 ∈ V )
13	10 12	xpexd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝐵 × 𝑆 ) ∈ V )
14	5 13	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑊 ∈ V )
15	14 14	xpexd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝑊 × 𝑊 ) ∈ V )
16		simprll	⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) ) → 𝑎 ∈ 𝑊 )
17		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) ) → 𝑏 ∈ 𝑊 )
18	16 17	opabssxpd	⊢ ( 𝜑 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } ⊆ ( 𝑊 × 𝑊 ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } ⊆ ( 𝑊 × 𝑊 ) )
20	15 19	ssexd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } ∈ V )
21	6 20	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ∼ ∈ V )
22		fvexd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) ∈ V )
23		fveq2	⊢ ( 𝑟 = 𝑅 → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
24	23	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) = ( ._r ‘ 𝑅 ) )
25	24 3	eqtr4di	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ._r ‘ 𝑟 ) = · )
26		fvexd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) ∈ V )
27		vex	⊢ 𝑠 ∈ V
28	27	a1i	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → 𝑠 ∈ V )
29	26 28	xpexd	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) ∈ V )
30		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
31	30	ad2antrr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
32	31 1	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( Base ‘ 𝑟 ) = 𝐵 )
33		simplr	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → 𝑠 = 𝑆 )
34	32 33	xpeq12d	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) = ( 𝐵 × 𝑆 ) )
35	34 5	eqtr4di	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ( ( Base ‘ 𝑟 ) × 𝑠 ) = 𝑊 )
36		simpr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑤 = 𝑊 )
37	36	eleq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊 ) )
38	36	eleq2d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊 ) )
39	37 38	anbi12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ↔ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) )
40	33	adantr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑠 = 𝑆 )
41		simplr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑥 = · )
42		eqidd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → 𝑡 = 𝑡 )
43		fveq2	⊢ ( 𝑟 = 𝑅 → ( -_g ‘ 𝑟 ) = ( -_g ‘ 𝑅 ) )
44	43	ad3antrrr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( -_g ‘ 𝑟 ) = ( -_g ‘ 𝑅 ) )
45	44 4	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( -_g ‘ 𝑟 ) = − )
46	41	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) = ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) )
47	41	oveqd	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) )
48	45 46 47	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) = ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) )
49	41 42 48	oveq123d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) )
50		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0_g ‘ 𝑟 ) = ( 0_g ‘ 𝑅 ) )
51	50	ad3antrrr	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 0_g ‘ 𝑟 ) = ( 0_g ‘ 𝑅 ) )
52	51 2	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( 0_g ‘ 𝑟 ) = 0 )
53	49 52	eqeq12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ↔ ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) )
54	40 53	rexeqbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ↔ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) )
55	39 54	anbi12d	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → ( ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) ↔ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) ) )
56	55	opabbidv	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ∧ ∃ 𝑡 ∈ 𝑆 ( 𝑡 · ( ( ( 1^st ‘ 𝑎 ) · ( 2^nd ‘ 𝑏 ) ) − ( ( 1^st ‘ 𝑏 ) · ( 2^nd ‘ 𝑎 ) ) ) ) = 0 ) } )
57	56 6	eqtr4di	⊢ ( ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊 ) → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) } = ∼ )
58	29 35 57	csbied2	⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ∧ 𝑥 = · ) → ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) } = ∼ )
59	22 25 58	csbied2	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) } = ∼ )
60		df-erl	⊢ ~_RL = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ⦋ ( ._r ‘ 𝑟 ) / 𝑥 ⦌ ⦋ ( ( Base ‘ 𝑟 ) × 𝑠 ) / 𝑤 ⦌ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤 ) ∧ ∃ 𝑡 ∈ 𝑠 ( 𝑡 𝑥 ( ( ( 1^st ‘ 𝑎 ) 𝑥 ( 2^nd ‘ 𝑏 ) ) ( -_g ‘ 𝑟 ) ( ( 1^st ‘ 𝑏 ) 𝑥 ( 2^nd ‘ 𝑎 ) ) ) ) = ( 0_g ‘ 𝑟 ) ) } )
61	59 60	ovmpoga	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ∼ ∈ V ) → ( 𝑅 ~_RL 𝑆 ) = ∼ )
62	8 12 21 61	syl3anc	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( 𝑅 ~_RL 𝑆 ) = ∼ )
63	60	reldmmpo	⊢ Rel dom ~_RL
64	63	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ~_RL 𝑆 ) = ∅ )
65	64	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝑅 ~_RL 𝑆 ) = ∅ )
66	6 18	eqsstrid	⊢ ( 𝜑 → ∼ ⊆ ( 𝑊 × 𝑊 ) )
67	66	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ∼ ⊆ ( 𝑊 × 𝑊 ) )
68		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
69	1 68	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
70	69	xpeq1d	⊢ ( ¬ 𝑅 ∈ V → ( 𝐵 × 𝑆 ) = ( ∅ × 𝑆 ) )
71		0xp	⊢ ( ∅ × 𝑆 ) = ∅
72	70 71	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ( 𝐵 × 𝑆 ) = ∅ )
73	5 72	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝑊 = ∅ )
74		id	⊢ ( 𝑊 = ∅ → 𝑊 = ∅ )
75	74 74	xpeq12d	⊢ ( 𝑊 = ∅ → ( 𝑊 × 𝑊 ) = ( ∅ × ∅ ) )
76		0xp	⊢ ( ∅ × ∅ ) = ∅
77	75 76	eqtrdi	⊢ ( 𝑊 = ∅ → ( 𝑊 × 𝑊 ) = ∅ )
78	73 77	syl	⊢ ( ¬ 𝑅 ∈ V → ( 𝑊 × 𝑊 ) = ∅ )
79	78	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝑊 × 𝑊 ) = ∅ )
80	67 79	sseqtrd	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ∼ ⊆ ∅ )
81		ss0	⊢ ( ∼ ⊆ ∅ → ∼ = ∅ )
82	80 81	syl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ∼ = ∅ )
83	65 82	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ V ) → ( 𝑅 ~_RL 𝑆 ) = ∼ )
84	62 83	pm2.61dan	⊢ ( 𝜑 → ( 𝑅 ~_RL 𝑆 ) = ∼ )

Metamath Proof Explorer

Theorem erlval

Proof