Theorem 2arwcatlem1

Description: Lemma for 2arwcat . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypothesis	2arwcatlem1.x	⊢ ( 𝑋 𝐻 𝑋 ) = { 0 , 1 }
Assertion	2arwcatlem1	⊢ ( ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ↔ ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem1.x	⊢ ( 𝑋 𝐻 𝑋 ) = { 0 , 1 }
2		df-3an	⊢ ( ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 )
4		velsn	⊢ ( 𝑦 ∈ { 𝑋 } ↔ 𝑦 = 𝑋 )
5	3 4	anbi12i	⊢ ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) )
6		velsn	⊢ ( 𝑧 ∈ { 𝑋 } ↔ 𝑧 = 𝑋 )
7		velsn	⊢ ( 𝑤 ∈ { 𝑋 } ↔ 𝑤 = 𝑋 )
8	6 7	anbi12i	⊢ ( ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ↔ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) )
9	5 8	anbi12i	⊢ ( ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ) ↔ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) )
10	9	anbi1i	⊢ ( ( ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
11		simpll	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → 𝑥 = 𝑋 )
12		simplr	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → 𝑦 = 𝑋 )
13	11 12	oveq12d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑋 ) )
14	13 1	eqtrdi	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑥 𝐻 𝑦 ) = { 0 , 1 } )
15	14	eleq2d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ { 0 , 1 } ) )
16		simprl	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → 𝑧 = 𝑋 )
17	12 16	oveq12d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑋 𝐻 𝑋 ) )
18	17 1	eqtrdi	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑦 𝐻 𝑧 ) = { 0 , 1 } )
19	18	eleq2d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ↔ 𝑔 ∈ { 0 , 1 } ) )
20		simprr	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → 𝑤 = 𝑋 )
21	16 20	oveq12d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑋 𝐻 𝑋 ) )
22	21 1	eqtrdi	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑧 𝐻 𝑤 ) = { 0 , 1 } )
23	22	eleq2d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ↔ 𝑘 ∈ { 0 , 1 } ) )
24	15 19 23	3anbi123d	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( 𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 } ) ) )
25		vex	⊢ 𝑓 ∈ V
26	25	elpr	⊢ ( 𝑓 ∈ { 0 , 1 } ↔ ( 𝑓 = 0 ∨ 𝑓 = 1 ) )
27		vex	⊢ 𝑔 ∈ V
28	27	elpr	⊢ ( 𝑔 ∈ { 0 , 1 } ↔ ( 𝑔 = 0 ∨ 𝑔 = 1 ) )
29		vex	⊢ 𝑘 ∈ V
30	29	elpr	⊢ ( 𝑘 ∈ { 0 , 1 } ↔ ( 𝑘 = 0 ∨ 𝑘 = 1 ) )
31	26 28 30	3anbi123i	⊢ ( ( 𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 } ) ↔ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) )
32	24 31	bitrdi	⊢ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) → ( ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ↔ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) )
33	32	pm5.32i	⊢ ( ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) )
34	2 10 33	3bitrri	⊢ ( ( ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑋 ) ∧ ( 𝑧 = 𝑋 ∧ 𝑤 = 𝑋 ) ) ∧ ( ( 𝑓 = 0 ∨ 𝑓 = 1 ) ∧ ( 𝑔 = 0 ∨ 𝑔 = 1 ) ∧ ( 𝑘 = 0 ∨ 𝑘 = 1 ) ) ) ↔ ( ( 𝑥 ∈ { 𝑋 } ∧ 𝑦 ∈ { 𝑋 } ) ∧ ( 𝑧 ∈ { 𝑋 } ∧ 𝑤 ∈ { 𝑋 } ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )