This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem el7g

Description: Members of a set with seven elements. Lemma for usgrexmpl2nb0 etc. (Contributed by AV, 9-Aug-2025)

		Ref	Expression
	Assertion	el7g	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ ( { 𝐴 } ∪ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) ↔ ( 𝑋 = 𝐴 ∨ ( ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝑋 ∈ ( { 𝐴 } ∪ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) ↔ ( 𝑋 ∈ { 𝐴 } ∨ 𝑋 ∈ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) )
2		elsng	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ { 𝐴 } ↔ 𝑋 = 𝐴 ) )
3		elun	⊢ ( 𝑋 ∈ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ↔ ( 𝑋 ∈ { 𝐵 , 𝐶 , 𝐷 } ∨ 𝑋 ∈ { 𝐸 , 𝐹 , 𝐺 } ) )
4		eltpg	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ { 𝐵 , 𝐶 , 𝐷 } ↔ ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ) )
5		eltpg	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ { 𝐸 , 𝐹 , 𝐺 } ↔ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) )
6	4 5	orbi12d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∈ { 𝐵 , 𝐶 , 𝐷 } ∨ 𝑋 ∈ { 𝐸 , 𝐹 , 𝐺 } ) ↔ ( ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) ) )
7	3 6	bitrid	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ↔ ( ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) ) )
8	2 7	orbi12d	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑋 ∈ { 𝐴 } ∨ 𝑋 ∈ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) ↔ ( 𝑋 = 𝐴 ∨ ( ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) ) ) )
9	1 8	bitrid	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ ( { 𝐴 } ∪ ( { 𝐵 , 𝐶 , 𝐷 } ∪ { 𝐸 , 𝐹 , 𝐺 } ) ) ↔ ( 𝑋 = 𝐴 ∨ ( ( 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ∨ 𝑋 = 𝐷 ) ∨ ( 𝑋 = 𝐸 ∨ 𝑋 = 𝐹 ∨ 𝑋 = 𝐺 ) ) ) ) )