Theorem 2arwcatlem1 49333

Description: Lemma for 2arwcat 49338. (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 1088	. 2 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
2		velsn 4615	. . . . 5 ⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋)
3		velsn 4615	. . . . 5 ⊢ (𝑦 ∈ {𝑋} ↔ 𝑦 = 𝑋)
4	2, 3	anbi12i 628	. . . 4 ⊢ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑋))
5		velsn 4615	. . . . 5 ⊢ (𝑧 ∈ {𝑋} ↔ 𝑧 = 𝑋)
6		velsn 4615	. . . . 5 ⊢ (𝑤 ∈ {𝑋} ↔ 𝑤 = 𝑋)
7	5, 6	anbi12i 628	. . . 4 ⊢ ((𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ↔ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋))
8	4, 7	anbi12i 628	. . 3 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ↔ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)))
9	8	anbi1i 624	. 2 ⊢ ((((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
10		simpll 766	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑥 = 𝑋)
11		simplr 768	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑦 = 𝑋)
12	10, 11	oveq12d 7418	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑋))
13		2arwcatlem1.x	. . . . . . 7 ⊢ (𝑋𝐻𝑋) = { 0 , 1 }
14	12, 13	eqtrdi 2785	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = { 0 , 1 })
15	14	eleq2d 2819	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ { 0 , 1 }))
16		simprl 770	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑧 = 𝑋)
17	11, 16	oveq12d 7418	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = (𝑋𝐻𝑋))
18	17, 13	eqtrdi 2785	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = { 0 , 1 })
19	18	eleq2d 2819	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ { 0 , 1 }))
20		simprr 772	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑤 = 𝑋)
21	16, 20	oveq12d 7418	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = (𝑋𝐻𝑋))
22	21, 13	eqtrdi 2785	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = { 0 , 1 })
23	22	eleq2d 2819	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ { 0 , 1 }))
24	15, 19, 23	3anbi123d 1437	. . . 4 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 })))
25		vex 3461	. . . . . 6 ⊢ 𝑓 ∈ V
26	25	elpr 4624	. . . . 5 ⊢ (𝑓 ∈ { 0 , 1 } ↔ (𝑓 = 0 ∨ 𝑓 = 1 ))
27		vex 3461	. . . . . 6 ⊢ 𝑔 ∈ V
28	27	elpr 4624	. . . . 5 ⊢ (𝑔 ∈ { 0 , 1 } ↔ (𝑔 = 0 ∨ 𝑔 = 1 ))
29		vex 3461	. . . . . 6 ⊢ 𝑘 ∈ V
30	29	elpr 4624	. . . . 5 ⊢ (𝑘 ∈ { 0 , 1 } ↔ (𝑘 = 0 ∨ 𝑘 = 1 ))
31	26, 28, 30	3anbi123i 1155	. . . 4 ⊢ ((𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 }) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 )))
32	24, 31	bitrdi 287	. . 3 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
33	32	pm5.32i 574	. 2 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))))
34	1, 9, 33	3bitrri 298	1 ⊢ ((((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ ((𝑓 = 0 ∨ 𝑓 = 1 ) ∧ (𝑔 = 0 ∨ 𝑔 = 1 ) ∧ (𝑘 = 0 ∨ 𝑘 = 1 ))) ↔ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  {csn 4599  {cpr 4601  (class class class)co 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-iota 6481  df-fv 6536  df-ov 7403

This theorem is referenced by:  2arwcat  49338