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

Metamath Proof Explorer

Theorem djuin

Description: The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022)

Ref Expression
Assertion djuin ( ( inl “ 𝐴 ) ∩ ( inr “ 𝐵 ) ) = ∅

Proof

Step Hyp Ref Expression
1 incom ⊢ ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ( ( inl “ 𝐴 ) ∩ ( inr “ 𝐵 ) )
2 imassrn ⊢ ( inr “ 𝐵 ) ⊆ ran inr
3 djurf1o ⊢ inr : V –1-1-onto→ ( { 1o } × V )
4 f1of ⊢ ( inr : V –1-1-onto→ ( { 1o } × V ) → inr : V ⟶ ( { 1o } × V ) )
5 frn ⊢ ( inr : V ⟶ ( { 1o } × V ) → ran inr ⊆ ( { 1o } × V ) )
6 3 4 5 mp2b ⊢ ran inr ⊆ ( { 1o } × V )
7 2 6 sstri ⊢ ( inr “ 𝐵 ) ⊆ ( { 1o } × V )
8 incom ⊢ ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) )
9 imassrn ⊢ ( inl “ 𝐴 ) ⊆ ran inl
10 djulf1o ⊢ inl : V –1-1-onto→ ( { ∅ } × V )
11 f1of ⊢ ( inl : V –1-1-onto→ ( { ∅ } × V ) → inl : V ⟶ ( { ∅ } × V ) )
12 frn ⊢ ( inl : V ⟶ ( { ∅ } × V ) → ran inl ⊆ ( { ∅ } × V ) )
13 10 11 12 mp2b ⊢ ran inl ⊆ ( { ∅ } × V )
14 9 13 sstri ⊢ ( inl “ 𝐴 ) ⊆ ( { ∅ } × V )
15 1n0 ⊢ 1o ≠ ∅
16 15 necomi ⊢ ∅ ≠ 1o
17 disjsn2 ⊢ ( ∅ ≠ 1o → ( { ∅ } ∩ { 1o } ) = ∅ )
18 xpdisj1 ⊢ ( ( { ∅ } ∩ { 1o } ) = ∅ → ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅ )
19 16 17 18 mp2b ⊢ ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅
20 ssdisj ⊢ ( ( ( inl “ 𝐴 ) ⊆ ( { ∅ } × V ) ∧ ( ( { ∅ } × V ) ∩ ( { 1o } × V ) ) = ∅ ) → ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ∅ )
21 14 19 20 mp2an ⊢ ( ( inl “ 𝐴 ) ∩ ( { 1o } × V ) ) = ∅
22 8 21 eqtr3i ⊢ ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) ) = ∅
23 ssdisj ⊢ ( ( ( inr “ 𝐵 ) ⊆ ( { 1o } × V ) ∧ ( ( { 1o } × V ) ∩ ( inl “ 𝐴 ) ) = ∅ ) → ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ∅ )
24 7 22 23 mp2an ⊢ ( ( inr “ 𝐵 ) ∩ ( inl “ 𝐴 ) ) = ∅
25 1 24 eqtr3i ⊢ ( ( inl “ 𝐴 ) ∩ ( inr “ 𝐵 ) ) = ∅