Theorem 2arwcatlem1 50216

Description: Lemma for 2arwcat 50221. (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 1100	. 2 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
2		velsn 4598	. . . . 5 ⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋)
3		velsn 4598	. . . . 5 ⊢ (𝑦 ∈ {𝑋} ↔ 𝑦 = 𝑋)
4	2, 3	anbi12i 637	. . . 4 ⊢ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑋))
5		velsn 4598	. . . . 5 ⊢ (𝑧 ∈ {𝑋} ↔ 𝑧 = 𝑋)
6		velsn 4598	. . . . 5 ⊢ (𝑤 ∈ {𝑋} ↔ 𝑤 = 𝑋)
7	5, 6	anbi12i 637	. . . 4 ⊢ ((𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ↔ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋))
8	4, 7	anbi12i 637	. . 3 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ↔ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)))
9	8	anbi1i 633	. 2 ⊢ ((((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
10		simpll 776	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑥 = 𝑋)
11		simplr 778	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑦 = 𝑋)
12	10, 11	oveq12d 7414	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑋))
13		2arwcatlem1.x	. . . . . . 7 ⊢ (𝑋𝐻𝑋) = { 0 , 1 }
14	12, 13	eqtrdi 2813	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = { 0 , 1 })
15	14	eleq2d 2848	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ { 0 , 1 }))
16		simprl 780	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑧 = 𝑋)
17	11, 16	oveq12d 7414	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = (𝑋𝐻𝑋))
18	17, 13	eqtrdi 2813	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = { 0 , 1 })
19	18	eleq2d 2848	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ { 0 , 1 }))
20		simprr 782	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑤 = 𝑋)
21	16, 20	oveq12d 7414	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = (𝑋𝐻𝑋))
22	21, 13	eqtrdi 2813	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = { 0 , 1 })
23	22	eleq2d 2848	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ { 0 , 1 }))
24	15, 19, 23	3anbi123d 1457	. . . 4 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 })))
25		vex 3458	. . . . . 6 ⊢ 𝑓 ∈ V
26	25	elpr 4607	. . . . 5 ⊢ (𝑓 ∈ { 0 , 1 } ↔ (𝑓 = 0 ∨ 𝑓 = 1 ))
27		vex 3458	. . . . . 6 ⊢ 𝑔 ∈ V
28	27	elpr 4607	. . . . 5 ⊢ (𝑔 ∈ { 0 , 1 } ↔ (𝑔 = 0 ∨ 𝑔 = 1 ))
29		vex 3458	. . . . . 6 ⊢ 𝑘 ∈ V
30	29	elpr 4607	. . . . 5 ⊢ (𝑘 ∈ { 0 , 1 } ↔ (𝑘 = 0 ∨ 𝑘 = 1 ))
31	26, 28, 30	3anbi123i 1168	. . . 4 ⊢ ((𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 }) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 )))
32	24, 31	bitrdi 289	. . 3 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
33	32	pm5.32i 582	. 2 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
34	1, 9, 33	3bitrri 300	1 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))

Syntax hints:   ↔ wb 208   ∧ wa 399   ∨ wo 858   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  {csn 4582  {cpr 4584  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  2arwcat  50221