djur

Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022)

		Ref	Expression
	Assertion	djur	⊢ ( 𝐶 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝐶 = ( inl ‘ 𝑥 ) ∨ ∃ 𝑥 ∈ 𝐵 𝐶 = ( inr ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) )
2	1	eleq2i	⊢ ( 𝐶 ∈ ( 𝐴 ⊔ 𝐵 ) ↔ 𝐶 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) ) )
3		elun	⊢ ( 𝐶 ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1_o } × 𝐵 ) ) ↔ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) ∨ 𝐶 ∈ ( { 1_o } × 𝐵 ) ) )
4	2 3	sylbb	⊢ ( 𝐶 ∈ ( 𝐴 ⊔ 𝐵 ) → ( 𝐶 ∈ ( { ∅ } × 𝐴 ) ∨ 𝐶 ∈ ( { 1_o } × 𝐵 ) ) )
5		xp2nd	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ( 2^nd ‘ 𝐶 ) ∈ 𝐴 )
6		1st2nd2	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ )
7		xp1st	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ( 1^st ‘ 𝐶 ) ∈ { ∅ } )
8		elsni	⊢ ( ( 1^st ‘ 𝐶 ) ∈ { ∅ } → ( 1^st ‘ 𝐶 ) = ∅ )
9		opeq1	⊢ ( ( 1^st ‘ 𝐶 ) = ∅ → ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ )
10	9	eqeq2d	⊢ ( ( 1^st ‘ 𝐶 ) = ∅ → ( 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ↔ 𝐶 = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ ) )
11	7 8 10	3syl	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ( 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ↔ 𝐶 = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ ) )
12	6 11	mpbid	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → 𝐶 = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ )
13		fvexd	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ( 2^nd ‘ 𝐶 ) ∈ V )
14		opex	⊢ ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ ∈ V
15		opeq2	⊢ ( 𝑦 = ( 2^nd ‘ 𝐶 ) → ⟨ ∅ , 𝑦 ⟩ = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ )
16		df-inl	⊢ inl = ( 𝑦 ∈ V ↦ ⟨ ∅ , 𝑦 ⟩ )
17	15 16	fvmptg	⊢ ( ( ( 2^nd ‘ 𝐶 ) ∈ V ∧ ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ ∈ V ) → ( inl ‘ ( 2^nd ‘ 𝐶 ) ) = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ )
18	13 14 17	sylancl	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ( inl ‘ ( 2^nd ‘ 𝐶 ) ) = ⟨ ∅ , ( 2^nd ‘ 𝐶 ) ⟩ )
19	12 18	eqtr4d	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → 𝐶 = ( inl ‘ ( 2^nd ‘ 𝐶 ) ) )
20		fveq2	⊢ ( 𝑥 = ( 2^nd ‘ 𝐶 ) → ( inl ‘ 𝑥 ) = ( inl ‘ ( 2^nd ‘ 𝐶 ) ) )
21	20	rspceeqv	⊢ ( ( ( 2^nd ‘ 𝐶 ) ∈ 𝐴 ∧ 𝐶 = ( inl ‘ ( 2^nd ‘ 𝐶 ) ) ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( inl ‘ 𝑥 ) )
22	5 19 21	syl2anc	⊢ ( 𝐶 ∈ ( { ∅ } × 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = ( inl ‘ 𝑥 ) )
23		xp2nd	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ( 2^nd ‘ 𝐶 ) ∈ 𝐵 )
24		1st2nd2	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ )
25		xp1st	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ( 1^st ‘ 𝐶 ) ∈ { 1_o } )
26		elsni	⊢ ( ( 1^st ‘ 𝐶 ) ∈ { 1_o } → ( 1^st ‘ 𝐶 ) = 1_o )
27		opeq1	⊢ ( ( 1^st ‘ 𝐶 ) = 1_o → ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ )
28	27	eqeq2d	⊢ ( ( 1^st ‘ 𝐶 ) = 1_o → ( 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ↔ 𝐶 = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ ) )
29	25 26 28	3syl	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ( 𝐶 = ⟨ ( 1^st ‘ 𝐶 ) , ( 2^nd ‘ 𝐶 ) ⟩ ↔ 𝐶 = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ ) )
30	24 29	mpbid	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → 𝐶 = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ )
31		fvexd	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ( 2^nd ‘ 𝐶 ) ∈ V )
32		opex	⊢ ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ ∈ V
33		opeq2	⊢ ( 𝑧 = ( 2^nd ‘ 𝐶 ) → ⟨ 1_o , 𝑧 ⟩ = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ )
34		df-inr	⊢ inr = ( 𝑧 ∈ V ↦ ⟨ 1_o , 𝑧 ⟩ )
35	33 34	fvmptg	⊢ ( ( ( 2^nd ‘ 𝐶 ) ∈ V ∧ ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ ∈ V ) → ( inr ‘ ( 2^nd ‘ 𝐶 ) ) = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ )
36	31 32 35	sylancl	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ( inr ‘ ( 2^nd ‘ 𝐶 ) ) = ⟨ 1_o , ( 2^nd ‘ 𝐶 ) ⟩ )
37	30 36	eqtr4d	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → 𝐶 = ( inr ‘ ( 2^nd ‘ 𝐶 ) ) )
38		fveq2	⊢ ( 𝑥 = ( 2^nd ‘ 𝐶 ) → ( inr ‘ 𝑥 ) = ( inr ‘ ( 2^nd ‘ 𝐶 ) ) )
39	38	rspceeqv	⊢ ( ( ( 2^nd ‘ 𝐶 ) ∈ 𝐵 ∧ 𝐶 = ( inr ‘ ( 2^nd ‘ 𝐶 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝐶 = ( inr ‘ 𝑥 ) )
40	23 37 39	syl2anc	⊢ ( 𝐶 ∈ ( { 1_o } × 𝐵 ) → ∃ 𝑥 ∈ 𝐵 𝐶 = ( inr ‘ 𝑥 ) )
41	22 40	orim12i	⊢ ( ( 𝐶 ∈ ( { ∅ } × 𝐴 ) ∨ 𝐶 ∈ ( { 1_o } × 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝐶 = ( inl ‘ 𝑥 ) ∨ ∃ 𝑥 ∈ 𝐵 𝐶 = ( inr ‘ 𝑥 ) ) )
42	4 41	syl	⊢ ( 𝐶 ∈ ( 𝐴 ⊔ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝐶 = ( inl ‘ 𝑥 ) ∨ ∃ 𝑥 ∈ 𝐵 𝐶 = ( inr ‘ 𝑥 ) ) )

Metamath Proof Explorer

Theorem djur

Proof