Theorem strle2

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

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

Proof

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