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

Metamath Proof Explorer

Theorem strle3

Description: Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypotheses strle1.i ⊢ 𝐼 ∈ ℕ
strle1.a ⊢ 𝐴 = 𝐼
strle2.j ⊢ 𝐼 < 𝐽
strle2.k ⊢ 𝐽 ∈ ℕ
strle2.b ⊢ 𝐵 = 𝐽
strle3.k ⊢ 𝐽 < 𝐾
strle3.l ⊢ 𝐾 ∈ ℕ
strle3.c ⊢ 𝐶 = 𝐾
Assertion strle3 { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } Struct ⟨ 𝐼 , 𝐾 ⟩

Proof

Step Hyp Ref Expression
1 strle1.i ⊢ 𝐼 ∈ ℕ
2 strle1.a ⊢ 𝐴 = 𝐼
3 strle2.j ⊢ 𝐼 < 𝐽
4 strle2.k ⊢ 𝐽 ∈ ℕ
5 strle2.b ⊢ 𝐵 = 𝐽
6 strle3.k ⊢ 𝐽 < 𝐾
7 strle3.l ⊢ 𝐾 ∈ ℕ
8 strle3.c ⊢ 𝐶 = 𝐾
9 df-tp ⊢ { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } = ( { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ } ∪ { ⟨ 𝐶 , 𝑍 ⟩ } )
10 1 2 3 4 5 strle2 ⊢ { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ } Struct ⟨ 𝐼 , 𝐽 ⟩
11 7 8 strle1 ⊢ { ⟨ 𝐶 , 𝑍 ⟩ } Struct ⟨ 𝐾 , 𝐾 ⟩
12 10 11 6 strleun ⊢ ( { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ } ∪ { ⟨ 𝐶 , 𝑍 ⟩ } ) Struct ⟨ 𝐼 , 𝐾 ⟩
13 9 12 eqbrtri ⊢ { ⟨ 𝐴 , 𝑋 ⟩ , ⟨ 𝐵 , 𝑌 ⟩ , ⟨ 𝐶 , 𝑍 ⟩ } Struct ⟨ 𝐼 , 𝐾 ⟩