Theorem 2arwcatlem1 50406

Description: Lemma for 2arwcat 50411. (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 1105	. 2 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
2		velsn 4610	. . . . 5 ⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋)
3		velsn 4610	. . . . 5 ⊢ (𝑦 ∈ {𝑋} ↔ 𝑦 = 𝑋)
4	2, 3	anbi12i 640	. . . 4 ⊢ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑋))
5		velsn 4610	. . . . 5 ⊢ (𝑧 ∈ {𝑋} ↔ 𝑧 = 𝑋)
6		velsn 4610	. . . . 5 ⊢ (𝑤 ∈ {𝑋} ↔ 𝑤 = 𝑋)
7	5, 6	anbi12i 640	. . . 4 ⊢ ((𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ↔ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋))
8	4, 7	anbi12i 640	. . 3 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ↔ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)))
9	8	anbi1i 636	. 2 ⊢ ((((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
10		simpll 779	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑥 = 𝑋)
11		simplr 781	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑦 = 𝑋)
12	10, 11	oveq12d 7441	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑋))
13		2arwcatlem1.x	. . . . . . 7 ⊢ (𝑋𝐻𝑋) = { 0 , 1 }
14	12, 13	eqtrdi 2817	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = { 0 , 1 })
15	14	eleq2d 2852	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ { 0 , 1 }))
16		simprl 783	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑧 = 𝑋)
17	11, 16	oveq12d 7441	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = (𝑋𝐻𝑋))
18	17, 13	eqtrdi 2817	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = { 0 , 1 })
19	18	eleq2d 2852	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ { 0 , 1 }))
20		simprr 785	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑤 = 𝑋)
21	16, 20	oveq12d 7441	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = (𝑋𝐻𝑋))
22	21, 13	eqtrdi 2817	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = { 0 , 1 })
23	22	eleq2d 2852	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ { 0 , 1 }))
24	15, 19, 23	3anbi123d 1464	. . . 4 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 })))
25		vex 3462	. . . . . 6 ⊢ 𝑓 ∈ V
26	25	elpr 4619	. . . . 5 ⊢ (𝑓 ∈ { 0 , 1 } ↔ (𝑓 = 0 ∨ 𝑓 = 1 ))
27		vex 3462	. . . . . 6 ⊢ 𝑔 ∈ V
28	27	elpr 4619	. . . . 5 ⊢ (𝑔 ∈ { 0 , 1 } ↔ (𝑔 = 0 ∨ 𝑔 = 1 ))
29		vex 3462	. . . . . 6 ⊢ 𝑘 ∈ V
30	29	elpr 4619	. . . . 5 ⊢ (𝑘 ∈ { 0 , 1 } ↔ (𝑘 = 0 ∨ 𝑘 = 1 ))
31	26, 28, 30	3anbi123i 1173	. . . 4 ⊢ ((𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 }) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 )))
32	24, 31	bitrdi 290	. . 3 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
33	32	pm5.32i 585	. 2 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
34	1, 9, 33	3bitrri 301	1 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  {csn 4594  {cpr 4596  (class class class)co 7423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  2arwcat  50411