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 ⟨ 𝐼 , 𝐾 ⟩