Theorem 2arwcatlem1 50085

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

Hypothesis

Ref	Expression
2arwcatlem1.x	⊢ (𝑋𝐻𝑋) = { 0 , 1 }

Assertion

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

Proof of Theorem 2arwcatlem1

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  {csn 4555  {cpr 4557  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  2arwcat  50090