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

Metamath Proof Explorer

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 } × ( 𝐴 ∪ 𝐵 ) )