Theorem 2arwcatlem1 49954

Description: Lemma for 2arwcat 49959. (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 1089	. 2 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
2		velsn 4598	. . . . 5 ⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋)
3		velsn 4598	. . . . 5 ⊢ (𝑦 ∈ {𝑋} ↔ 𝑦 = 𝑋)
4	2, 3	anbi12i 629	. . . 4 ⊢ ((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑋))
5		velsn 4598	. . . . 5 ⊢ (𝑧 ∈ {𝑋} ↔ 𝑧 = 𝑋)
6		velsn 4598	. . . . 5 ⊢ (𝑤 ∈ {𝑋} ↔ 𝑤 = 𝑋)
7	5, 6	anbi12i 629	. . . 4 ⊢ ((𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋}) ↔ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋))
8	4, 7	anbi12i 629	. . 3 ⊢ (((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ↔ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)))
9	8	anbi1i 625	. 2 ⊢ ((((𝑥 ∈ {𝑋} ∧ 𝑦 ∈ {𝑋}) ∧ (𝑧 ∈ {𝑋} ∧ 𝑤 ∈ {𝑋})) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))) ↔ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) ∧ (𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤))))
10		simpll 767	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑥 = 𝑋)
11		simplr 769	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑦 = 𝑋)
12	10, 11	oveq12d 7386	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑋))
13		2arwcatlem1.x	. . . . . . 7 ⊢ (𝑋𝐻𝑋) = { 0 , 1 }
14	12, 13	eqtrdi 2788	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑥𝐻𝑦) = { 0 , 1 })
15	14	eleq2d 2823	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑓 ∈ (𝑥𝐻𝑦) ↔ 𝑓 ∈ { 0 , 1 }))
16		simprl 771	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑧 = 𝑋)
17	11, 16	oveq12d 7386	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = (𝑋𝐻𝑋))
18	17, 13	eqtrdi 2788	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑦𝐻𝑧) = { 0 , 1 })
19	18	eleq2d 2823	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑔 ∈ (𝑦𝐻𝑧) ↔ 𝑔 ∈ { 0 , 1 }))
20		simprr 773	. . . . . . . 8 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → 𝑤 = 𝑋)
21	16, 20	oveq12d 7386	. . . . . . 7 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = (𝑋𝐻𝑋))
22	21, 13	eqtrdi 2788	. . . . . 6 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑧𝐻𝑤) = { 0 , 1 })
23	22	eleq2d 2823	. . . . 5 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → (𝑘 ∈ (𝑧𝐻𝑤) ↔ 𝑘 ∈ { 0 , 1 }))
24	15, 19, 23	3anbi123d 1439	. . . 4 ⊢ (((𝑥 = 𝑋 ∧ 𝑦 = 𝑋) ∧ (𝑧 = 𝑋 ∧ 𝑤 = 𝑋)) → ((𝑓 ∈ (𝑥𝐻𝑦) ∧ 𝑔 ∈ (𝑦𝐻𝑧) ∧ 𝑘 ∈ (𝑧𝐻𝑤)) ↔ (𝑓 ∈ { 0 , 1 } ∧ 𝑔 ∈ { 0 , 1 } ∧ 𝑘 ∈ { 0 , 1 })))
25		vex 3446	. . . . . 6 ⊢ 𝑓 ∈ V
26	25	elpr 4607	. . . . 5 ⊢ (𝑓 ∈ { 0 , 1 } ↔ (𝑓 = 0 ∨ 𝑓 = 1 ))
27		vex 3446	. . . . . 6 ⊢ 𝑔 ∈ V
28	27	elpr 4607	. . . . 5 ⊢ (𝑔 ∈ { 0 , 1 } ↔ (𝑔 = 0 ∨ 𝑔 = 1 ))
29		vex 3446	. . . . . 6 ⊢ 𝑘 ∈ V
30	29	elpr 4607	. . . . 5 ⊢ (𝑘 ∈ { 0 , 1 } ↔ (𝑘 = 0 ∨ 𝑘 = 1 ))
31	26, 28, 30	3anbi123i 1156	. . . 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 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {csn 4582  {cpr 4584  (class class class)co 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  2arwcat  49959