Theorem 2arwcatlem4

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

	Ref	Expression
Hypotheses	2arwcatlem2.a	$$⊢\phi \to A=X$$
	2arwcatlem2.b	$$⊢\phi \to B=Y$$
	2arwcatlem2.c	$$⊢\phi \to C=Z$$
	2arwcatlem2.f	$$⊢\phi \to \left(F=\underset{\dot{}}{0}\vee F=\underset{\dot{}}{1}\right)$$
	2arwcatlem2.1	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
	2arwcatlem3.0	$$⊢\phi \to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
	2arwcatlem4.0	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
	2arwcatlem4.00	$$⊢\phi \to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
	2arwcatlem4.g	$$⊢\phi \to \left(G=\underset{\dot{}}{0}\vee G=\underset{\dot{}}{1}\right)$$
Assertion	2arwcatlem4	$$⊢\phi \to G\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem2.a	$$⊢\phi \to A=X$$
2		2arwcatlem2.b	$$⊢\phi \to B=Y$$
3		2arwcatlem2.c	$$⊢\phi \to C=Z$$
4		2arwcatlem2.f	$$⊢\phi \to \left(F=\underset{\dot{}}{0}\vee F=\underset{\dot{}}{1}\right)$$
5		2arwcatlem2.1	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
6		2arwcatlem3.0	$$⊢\phi \to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
7		2arwcatlem4.0	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
8		2arwcatlem4.00	$$⊢\phi \to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
9		2arwcatlem4.g	$$⊢\phi \to \left(G=\underset{\dot{}}{0}\vee G=\underset{\dot{}}{1}\right)$$
10	1 2	opeq12d	$$⊢\phi \to ⟨A,B⟩=⟨X,Y⟩$$
11	10 3	oveq12d	$$⊢\phi \to ⟨A,B⟩\underset{\dot{}}{·}C=⟨X,Y⟩\underset{\dot{}}{·}Z$$
12	11	oveqd	$$⊢\phi \to G\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F=G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F$$
13		simpr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{0}\right)\to G=\underset{\dot{}}{0}$$
14		simplr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{0}\right)\to F=\underset{\dot{}}{0}$$
15	13 14	oveq12d	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}$$
16	8	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
17	15 16	eqeltrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
18		simpr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to G=\underset{\dot{}}{1}$$
19		simplr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to F=\underset{\dot{}}{0}$$
20	18 19	oveq12d	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}$$
21	7	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
22	20 21	eqtrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{0}$$
23		ovex	$$⊢\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{0}\in \mathrm{V}$$
24	7 23	eqeltrrdi	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
25		prid1g	$$⊢\underset{\dot{}}{0}\in \mathrm{V}\to \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
26	24 25	syl	$$⊢\phi \to \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
27	26	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
28	22 27	eqeltrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{0}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
29	9	adantr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to \left(G=\underset{\dot{}}{0}\vee G=\underset{\dot{}}{1}\right)$$
30	17 28 29	mpjaodan	$$⊢\left(\phi \wedge F=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
31		simpr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to G=\underset{\dot{}}{0}$$
32		simplr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to F=\underset{\dot{}}{1}$$
33	31 32	oveq12d	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}$$
34	6	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{0}$$
35	33 34	eqtrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{0}$$
36	26	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{0}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
37	35 36	eqeltrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{0}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
38		simpr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to G=\underset{\dot{}}{1}$$
39		simplr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to F=\underset{\dot{}}{1}$$
40	38 39	oveq12d	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}$$
41	5	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
42	40 41	eqtrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F=\underset{\dot{}}{1}$$
43		ovex	$$⊢\underset{\dot{}}{1}\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)\underset{\dot{}}{1}\in \mathrm{V}$$
44	5 43	eqeltrrdi	$$⊢\phi \to \underset{\dot{}}{1}\in \mathrm{V}$$
45		prid2g	$$⊢\underset{\dot{}}{1}\in \mathrm{V}\to \underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
46	44 45	syl	$$⊢\phi \to \underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
47	46	ad2antrr	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to \underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
48	42 47	eqeltrd	$$⊢\left(\left(\phi \wedge F=\underset{\dot{}}{1}\right)\wedge G=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
49	9	adantr	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to \left(G=\underset{\dot{}}{0}\vee G=\underset{\dot{}}{1}\right)$$
50	37 48 49	mpjaodan	$$⊢\left(\phi \wedge F=\underset{\dot{}}{1}\right)\to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
51	30 50 4	mpjaodan	$$⊢\phi \to G\left(⟨X,Y⟩\underset{\dot{}}{·}Z\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$
52	12 51	eqeltrd	$$⊢\phi \to G\left(⟨A,B⟩\underset{\dot{}}{·}C\right)F\in \left\{\underset{\dot{}}{0},\underset{\dot{}}{1}\right\}$$