Theorem djuss

Description: A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022)

	Ref	Expression
Assertion	djuss	⊢ ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		djur	⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) ) )
2		simpr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → 𝑥 = ( inl ‘ 𝑦 ) )
3		df-inl	⊢ inl = ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )
4		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , 𝑦 ⟩ )
5		elex	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ V )
6		opex	⊢ ⟨ ∅ , 𝑦 ⟩ ∈ V
7	6	a1i	⊢ ( 𝑦 ∈ 𝐴 → ⟨ ∅ , 𝑦 ⟩ ∈ V )
8	3 4 5 7	fvmptd3	⊢ ( 𝑦 ∈ 𝐴 → ( inl ‘ 𝑦 ) = ⟨ ∅ , 𝑦 ⟩ )
9	8	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → ( inl ‘ 𝑦 ) = ⟨ ∅ , 𝑦 ⟩ )
10	2 9	eqtrd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → 𝑥 = ⟨ ∅ , 𝑦 ⟩ )
11		elun1	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) )
12		0ex	⊢ ∅ ∈ V
13	12	prid1	⊢ ∅ ∈ { ∅ , 1o }
14	11 13	jctil	⊢ ( 𝑦 ∈ 𝐴 → ( ∅ ∈ { ∅ , 1o } ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
15	14	adantr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → ( ∅ ∈ { ∅ , 1o } ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
16		opelxp	⊢ ( ⟨ ∅ , 𝑦 ⟩ ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) ↔ ( ∅ ∈ { ∅ , 1o } ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
17	15 16	sylibr	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → ⟨ ∅ , 𝑦 ⟩ ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
18	10 17	eqeltrd	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
19	18	rexlimiva	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
20		simpr	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑥 = ( inr ‘ 𝑦 ) )
21		df-inr	⊢ inr = ( 𝑥 ∈ V ↦ ⟨ 1o , 𝑥 ⟩ )
22		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ 1o , 𝑥 ⟩ = ⟨ 1o , 𝑦 ⟩ )
23		elex	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ V )
24		opex	⊢ ⟨ 1o , 𝑦 ⟩ ∈ V
25	24	a1i	⊢ ( 𝑦 ∈ 𝐵 → ⟨ 1o , 𝑦 ⟩ ∈ V )
26	21 22 23 25	fvmptd3	⊢ ( 𝑦 ∈ 𝐵 → ( inr ‘ 𝑦 ) = ⟨ 1o , 𝑦 ⟩ )
27	26	adantr	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → ( inr ‘ 𝑦 ) = ⟨ 1o , 𝑦 ⟩ )
28	20 27	eqtrd	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑥 = ⟨ 1o , 𝑦 ⟩ )
29		elun2	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) )
30	29	adantr	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) )
31		1oex	⊢ 1o ∈ V
32	31	prid2	⊢ 1o ∈ { ∅ , 1o }
33	30 32	jctil	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → ( 1o ∈ { ∅ , 1o } ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
34		opelxp	⊢ ( ⟨ 1o , 𝑦 ⟩ ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) ↔ ( 1o ∈ { ∅ , 1o } ∧ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ) )
35	33 34	sylibr	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → ⟨ 1o , 𝑦 ⟩ ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
36	28 35	eqeltrd	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
37	36	rexlimiva	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
38	19 37	jaoi	⊢ ( ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
39	1 38	syl	⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → 𝑥 ∈ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) ) )
40	39	ssriv	⊢ ( 𝐴 ⊔ 𝐵 ) ⊆ ( { ∅ , 1o } × ( 𝐴 ∪ 𝐵 ) )