Metamath Proof Explorer

Theorem djuun

Description: The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022)

Ref Expression
Assertion djuun ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) = ( 𝐴 ⊔ 𝐵 )

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑥 ∈ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) ↔ ( 𝑥 ∈ ( inl “ 𝐴 ) ∨ 𝑥 ∈ ( inr “ 𝐵 ) ) )
2 djulf1o ⊢ inl : V –1-1-onto→ ( { ∅ } × V )
3 f1ofn ⊢ ( inl : V –1-1-onto→ ( { ∅ } × V ) → inl Fn V )
4 2 3 ax-mp ⊢ inl Fn V
5 ssv ⊢ 𝐴 ⊆ V
6 fvelimab ⊢ ( ( inl Fn V ∧ 𝐴 ⊆ V ) → ( 𝑥 ∈ ( inl “ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐴 ( inl ‘ 𝑢 ) = 𝑥 ) )
7 4 5 6 mp2an ⊢ ( 𝑥 ∈ ( inl “ 𝐴 ) ↔ ∃ 𝑢 ∈ 𝐴 ( inl ‘ 𝑢 ) = 𝑥 )
8 7 biimpi ⊢ ( 𝑥 ∈ ( inl “ 𝐴 ) → ∃ 𝑢 ∈ 𝐴 ( inl ‘ 𝑢 ) = 𝑥 )
9 simprr ⊢ ( ( 𝑥 ∈ ( inl “ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( inl ‘ 𝑢 ) = 𝑥 ) ) → ( inl ‘ 𝑢 ) = 𝑥 )
10 vex ⊢ 𝑢 ∈ V
11 opex ⊢ ⟨ ∅ , 𝑢 ⟩ ∈ V
12 opeq2 ⊢ ( 𝑧 = 𝑢 → ⟨ ∅ , 𝑧 ⟩ = ⟨ ∅ , 𝑢 ⟩ )
13 df-inl ⊢ inl = ( 𝑧 ∈ V ↦ ⟨ ∅ , 𝑧 ⟩ )
14 12 13 fvmptg ⊢ ( ( 𝑢 ∈ V ∧ ⟨ ∅ , 𝑢 ⟩ ∈ V ) → ( inl ‘ 𝑢 ) = ⟨ ∅ , 𝑢 ⟩ )
15 10 11 14 mp2an ⊢ ( inl ‘ 𝑢 ) = ⟨ ∅ , 𝑢 ⟩
16 0ex ⊢ ∅ ∈ V
17 16 snid ⊢ ∅ ∈ { ∅ }
18 opelxpi ⊢ ( ( ∅ ∈ { ∅ } ∧ 𝑢 ∈ 𝐴 ) → ⟨ ∅ , 𝑢 ⟩ ∈ ( { ∅ } × 𝐴 ) )
19 17 18 mpan ⊢ ( 𝑢 ∈ 𝐴 → ⟨ ∅ , 𝑢 ⟩ ∈ ( { ∅ } × 𝐴 ) )
20 19 ad2antrl ⊢ ( ( 𝑥 ∈ ( inl “ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( inl ‘ 𝑢 ) = 𝑥 ) ) → ⟨ ∅ , 𝑢 ⟩ ∈ ( { ∅ } × 𝐴 ) )
21 15 20 eqeltrid ⊢ ( ( 𝑥 ∈ ( inl “ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( inl ‘ 𝑢 ) = 𝑥 ) ) → ( inl ‘ 𝑢 ) ∈ ( { ∅ } × 𝐴 ) )
22 9 21 eqeltrrd ⊢ ( ( 𝑥 ∈ ( inl “ 𝐴 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( inl ‘ 𝑢 ) = 𝑥 ) ) → 𝑥 ∈ ( { ∅ } × 𝐴 ) )
23 8 22 rexlimddv ⊢ ( 𝑥 ∈ ( inl “ 𝐴 ) → 𝑥 ∈ ( { ∅ } × 𝐴 ) )
24 elun1 ⊢ ( 𝑥 ∈ ( { ∅ } × 𝐴 ) → 𝑥 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
25 23 24 syl ⊢ ( 𝑥 ∈ ( inl “ 𝐴 ) → 𝑥 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
26 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
27 25 26 eleqtrrdi ⊢ ( 𝑥 ∈ ( inl “ 𝐴 ) → 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) )
28 djurf1o ⊢ inr : V –1-1-onto→ ( { 1o } × V )
29 f1ofn ⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → inr Fn V )
30 28 29 ax-mp ⊢ inr Fn V
31 ssv ⊢ 𝐵 ⊆ V
32 fvelimab ⊢ ( ( inr Fn V ∧ 𝐵 ⊆ V ) → ( 𝑥 ∈ ( inr “ 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐵 ( inr ‘ 𝑢 ) = 𝑥 ) )
33 30 31 32 mp2an ⊢ ( 𝑥 ∈ ( inr “ 𝐵 ) ↔ ∃ 𝑢 ∈ 𝐵 ( inr ‘ 𝑢 ) = 𝑥 )
34 33 biimpi ⊢ ( 𝑥 ∈ ( inr “ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 ( inr ‘ 𝑢 ) = 𝑥 )
35 simprr ⊢ ( ( 𝑥 ∈ ( inr “ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ ( inr ‘ 𝑢 ) = 𝑥 ) ) → ( inr ‘ 𝑢 ) = 𝑥 )
36 opex ⊢ ⟨ 1o , 𝑢 ⟩ ∈ V
37 opeq2 ⊢ ( 𝑧 = 𝑢 → ⟨ 1o , 𝑧 ⟩ = ⟨ 1o , 𝑢 ⟩ )
38 df-inr ⊢ inr = ( 𝑧 ∈ V ↦ ⟨ 1o , 𝑧 ⟩ )
39 37 38 fvmptg ⊢ ( ( 𝑢 ∈ V ∧ ⟨ 1o , 𝑢 ⟩ ∈ V ) → ( inr ‘ 𝑢 ) = ⟨ 1o , 𝑢 ⟩ )
40 10 36 39 mp2an ⊢ ( inr ‘ 𝑢 ) = ⟨ 1o , 𝑢 ⟩
41 1oex ⊢ 1o ∈ V
42 41 snid ⊢ 1o ∈ { 1o }
43 opelxpi ⊢ ( ( 1o ∈ { 1o } ∧ 𝑢 ∈ 𝐵 ) → ⟨ 1o , 𝑢 ⟩ ∈ ( { 1o } × 𝐵 ) )
44 42 43 mpan ⊢ ( 𝑢 ∈ 𝐵 → ⟨ 1o , 𝑢 ⟩ ∈ ( { 1o } × 𝐵 ) )
45 44 ad2antrl ⊢ ( ( 𝑥 ∈ ( inr “ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ ( inr ‘ 𝑢 ) = 𝑥 ) ) → ⟨ 1o , 𝑢 ⟩ ∈ ( { 1o } × 𝐵 ) )
46 40 45 eqeltrid ⊢ ( ( 𝑥 ∈ ( inr “ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ ( inr ‘ 𝑢 ) = 𝑥 ) ) → ( inr ‘ 𝑢 ) ∈ ( { 1o } × 𝐵 ) )
47 35 46 eqeltrrd ⊢ ( ( 𝑥 ∈ ( inr “ 𝐵 ) ∧ ( 𝑢 ∈ 𝐵 ∧ ( inr ‘ 𝑢 ) = 𝑥 ) ) → 𝑥 ∈ ( { 1o } × 𝐵 ) )
48 34 47 rexlimddv ⊢ ( 𝑥 ∈ ( inr “ 𝐵 ) → 𝑥 ∈ ( { 1o } × 𝐵 ) )
49 elun2 ⊢ ( 𝑥 ∈ ( { 1o } × 𝐵 ) → 𝑥 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
50 48 49 syl ⊢ ( 𝑥 ∈ ( inr “ 𝐵 ) → 𝑥 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
51 50 26 eleqtrrdi ⊢ ( 𝑥 ∈ ( inr “ 𝐵 ) → 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) )
52 27 51 jaoi ⊢ ( ( 𝑥 ∈ ( inl “ 𝐴 ) ∨ 𝑥 ∈ ( inr “ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) )
53 1 52 sylbi ⊢ ( 𝑥 ∈ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) )
54 53 ssriv ⊢ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) ⊆ ( 𝐴 ⊔ 𝐵 )
55 djur ⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) ) )
56 vex ⊢ 𝑦 ∈ V
57 f1odm ⊢ ( inl : V –1-1-onto→ ( { ∅ } × V ) → dom inl = V )
58 2 57 ax-mp ⊢ dom inl = V
59 56 58 eleqtrri ⊢ 𝑦 ∈ dom inl
60 simpl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → 𝑦 ∈ 𝐴 )
61 13 funmpt2 ⊢ Fun inl
62 funfvima ⊢ ( ( Fun inl ∧ 𝑦 ∈ dom inl ) → ( 𝑦 ∈ 𝐴 → ( inl ‘ 𝑦 ) ∈ ( inl “ 𝐴 ) ) )
63 61 62 mpan ⊢ ( 𝑦 ∈ dom inl → ( 𝑦 ∈ 𝐴 → ( inl ‘ 𝑦 ) ∈ ( inl “ 𝐴 ) ) )
64 59 60 63 mpsyl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → ( inl ‘ 𝑦 ) ∈ ( inl “ 𝐴 ) )
65 eleq1 ⊢ ( 𝑥 = ( inl ‘ 𝑦 ) → ( 𝑥 ∈ ( inl “ 𝐴 ) ↔ ( inl ‘ 𝑦 ) ∈ ( inl “ 𝐴 ) ) )
66 65 adantl ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → ( 𝑥 ∈ ( inl “ 𝐴 ) ↔ ( inl ‘ 𝑦 ) ∈ ( inl “ 𝐴 ) ) )
67 64 66 mpbird ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ( inl ‘ 𝑦 ) ) → 𝑥 ∈ ( inl “ 𝐴 ) )
68 67 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) → 𝑥 ∈ ( inl “ 𝐴 ) )
69 f1odm ⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → dom inr = V )
70 28 69 ax-mp ⊢ dom inr = V
71 56 70 eleqtrri ⊢ 𝑦 ∈ dom inr
72 simpl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑦 ∈ 𝐵 )
73 f1ofun ⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → Fun inr )
74 28 73 ax-mp ⊢ Fun inr
75 funfvima ⊢ ( ( Fun inr ∧ 𝑦 ∈ dom inr ) → ( 𝑦 ∈ 𝐵 → ( inr ‘ 𝑦 ) ∈ ( inr “ 𝐵 ) ) )
76 74 75 mpan ⊢ ( 𝑦 ∈ dom inr → ( 𝑦 ∈ 𝐵 → ( inr ‘ 𝑦 ) ∈ ( inr “ 𝐵 ) ) )
77 71 72 76 mpsyl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → ( inr ‘ 𝑦 ) ∈ ( inr “ 𝐵 ) )
78 eleq1 ⊢ ( 𝑥 = ( inr ‘ 𝑦 ) → ( 𝑥 ∈ ( inr “ 𝐵 ) ↔ ( inr ‘ 𝑦 ) ∈ ( inr “ 𝐵 ) ) )
79 78 adantl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → ( 𝑥 ∈ ( inr “ 𝐵 ) ↔ ( inr ‘ 𝑦 ) ∈ ( inr “ 𝐵 ) ) )
80 77 79 mpbird ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = ( inr ‘ 𝑦 ) ) → 𝑥 ∈ ( inr “ 𝐵 ) )
81 80 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) → 𝑥 ∈ ( inr “ 𝐵 ) )
82 68 81 orim12i ⊢ ( ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( inl ‘ 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐵 𝑥 = ( inr ‘ 𝑦 ) ) → ( 𝑥 ∈ ( inl “ 𝐴 ) ∨ 𝑥 ∈ ( inr “ 𝐵 ) ) )
83 55 82 syl ⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → ( 𝑥 ∈ ( inl “ 𝐴 ) ∨ 𝑥 ∈ ( inr “ 𝐵 ) ) )
84 83 1 sylibr ⊢ ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) → 𝑥 ∈ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) )
85 84 ssriv ⊢ ( 𝐴 ⊔ 𝐵 ) ⊆ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) )
86 54 85 eqssi ⊢ ( ( inl “ 𝐴 ) ∪ ( inr “ 𝐵 ) ) = ( 𝐴 ⊔ 𝐵 )