Theorem 2arwcatlem1

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

	Ref	Expression
Hypothesis	2arwcatlem1.x	|- ( X H X ) = { .0. , .1. }
Assertion	2arwcatlem1	|- ( ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) <-> ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem1.x	|- ( X H X ) = { .0. , .1. }
2		df-3an	|- ( ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
3		velsn	|- ( x e. { X } <-> x = X )
4		velsn	|- ( y e. { X } <-> y = X )
5	3 4	anbi12i	|- ( ( x e. { X } /\ y e. { X } ) <-> ( x = X /\ y = X ) )
6		velsn	|- ( z e. { X } <-> z = X )
7		velsn	|- ( w e. { X } <-> w = X )
8	6 7	anbi12i	|- ( ( z e. { X } /\ w e. { X } ) <-> ( z = X /\ w = X ) )
9	5 8	anbi12i	|- ( ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) ) <-> ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) )
10	9	anbi1i	|- ( ( ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
11		simpll	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> x = X )
12		simplr	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> y = X )
13	11 12	oveq12d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( x H y ) = ( X H X ) )
14	13 1	eqtrdi	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( x H y ) = { .0. , .1. } )
15	14	eleq2d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( f e. ( x H y ) <-> f e. { .0. , .1. } ) )
16		simprl	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> z = X )
17	12 16	oveq12d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( y H z ) = ( X H X ) )
18	17 1	eqtrdi	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( y H z ) = { .0. , .1. } )
19	18	eleq2d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( g e. ( y H z ) <-> g e. { .0. , .1. } ) )
20		simprr	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> w = X )
21	16 20	oveq12d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( z H w ) = ( X H X ) )
22	21 1	eqtrdi	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( z H w ) = { .0. , .1. } )
23	22	eleq2d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( k e. ( z H w ) <-> k e. { .0. , .1. } ) )
24	15 19 23	3anbi123d	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( f e. { .0. , .1. } /\ g e. { .0. , .1. } /\ k e. { .0. , .1. } ) ) )
25		vex	|- f e. _V
26	25	elpr	|- ( f e. { .0. , .1. } <-> ( f = .0. \/ f = .1. ) )
27		vex	|- g e. _V
28	27	elpr	|- ( g e. { .0. , .1. } <-> ( g = .0. \/ g = .1. ) )
29		vex	|- k e. _V
30	29	elpr	|- ( k e. { .0. , .1. } <-> ( k = .0. \/ k = .1. ) )
31	26 28 30	3anbi123i	|- ( ( f e. { .0. , .1. } /\ g e. { .0. , .1. } /\ k e. { .0. , .1. } ) <-> ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) )
32	24 31	bitrdi	|- ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) -> ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) )
33	32	pm5.32i	|- ( ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) )
34	2 10 33	3bitrri	|- ( ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) <-> ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )