eldju2ndl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > eldju2ndl		GIF version

Theorem eldju2ndl 6907

Description: The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.)

**Assertion**
Ref	Expression
eldju2ndl	⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^st ‘𝑋) = ∅) → (2^nd ‘𝑋) ∈ 𝐴)

**Proof of Theorem eldju2ndl**
Step	Hyp	Ref	Expression
1		df-dju 6873	. . . . 5 ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1_o} × 𝐵))
2	1	eleq2i 2179	. . . 4 ⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) ↔ 𝑋 ∈ (({∅} × 𝐴) ∪ ({1_o} × 𝐵)))
3		elun 3181	. . . 4 ⊢ (𝑋 ∈ (({∅} × 𝐴) ∪ ({1_o} × 𝐵)) ↔ (𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1_o} × 𝐵)))
4	2, 3	bitri 183	. . 3 ⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) ↔ (𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1_o} × 𝐵)))
5		elxp6 6019	. . . . 5 ⊢ (𝑋 ∈ ({∅} × 𝐴) ↔ (𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩ ∧ ((1^st ‘𝑋) ∈ {∅} ∧ (2^nd ‘𝑋) ∈ 𝐴)))
6		simprr 504	. . . . . 6 ⊢ ((𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩ ∧ ((1^st ‘𝑋) ∈ {∅} ∧ (2^nd ‘𝑋) ∈ 𝐴)) → (2^nd ‘𝑋) ∈ 𝐴)
7	6	a1d 22	. . . . 5 ⊢ ((𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩ ∧ ((1^st ‘𝑋) ∈ {∅} ∧ (2^nd ‘𝑋) ∈ 𝐴)) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
8	5, 7	sylbi 120	. . . 4 ⊢ (𝑋 ∈ ({∅} × 𝐴) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
9		elxp6 6019	. . . . 5 ⊢ (𝑋 ∈ ({1_o} × 𝐵) ↔ (𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩ ∧ ((1^st ‘𝑋) ∈ {1_o} ∧ (2^nd ‘𝑋) ∈ 𝐵)))
10		elsni 3509	. . . . . . 7 ⊢ ((1^st ‘𝑋) ∈ {1_o} → (1^st ‘𝑋) = 1_o)
11		1n0 6281	. . . . . . . 8 ⊢ 1_o ≠ ∅
12		neeq1 2293	. . . . . . . 8 ⊢ ((1^st ‘𝑋) = 1_o → ((1^st ‘𝑋) ≠ ∅ ↔ 1_o ≠ ∅))
13	11, 12	mpbiri 167	. . . . . . 7 ⊢ ((1^st ‘𝑋) = 1_o → (1^st ‘𝑋) ≠ ∅)
14		eqneqall 2290	. . . . . . . 8 ⊢ ((1^st ‘𝑋) = ∅ → ((1^st ‘𝑋) ≠ ∅ → (2^nd ‘𝑋) ∈ 𝐴))
15	14	com12 30	. . . . . . 7 ⊢ ((1^st ‘𝑋) ≠ ∅ → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
16	10, 13, 15	3syl 17	. . . . . 6 ⊢ ((1^st ‘𝑋) ∈ {1_o} → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
17	16	ad2antrl 479	. . . . 5 ⊢ ((𝑋 = ⟨(1^st ‘𝑋), (2^nd ‘𝑋)⟩ ∧ ((1^st ‘𝑋) ∈ {1_o} ∧ (2^nd ‘𝑋) ∈ 𝐵)) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
18	9, 17	sylbi 120	. . . 4 ⊢ (𝑋 ∈ ({1_o} × 𝐵) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
19	8, 18	jaoi 688	. . 3 ⊢ ((𝑋 ∈ ({∅} × 𝐴) ∨ 𝑋 ∈ ({1_o} × 𝐵)) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
20	4, 19	sylbi 120	. 2 ⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1^st ‘𝑋) = ∅ → (2^nd ‘𝑋) ∈ 𝐴))
21	20	imp 123	1 ⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1^st ‘𝑋) = ∅) → (2^nd ‘𝑋) ∈ 𝐴)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ∨ wo 680 = wceq 1312 ∈ wcel 1461 ≠ wne 2280 ∪ cun 3033 ∅c0 3327 {csn 3491 ⟨cop 3494 × cxp 4495 ‘cfv 5079 1^st c1st 5988 2^nd c2nd 5989 1_oc1o 6258 ⊔ cdju 6872

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-13 1472 ax-14 1473 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-nul 4012 ax-pow 4056 ax-pr 4089 ax-un 4313

This theorem depends on definitions: df-bi 116 df-3an 945 df-tru 1315 df-nf 1418 df-sb 1717 df-eu 1976 df-mo 1977 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ne 2281 df-ral 2393 df-rex 2394 df-v 2657 df-sbc 2877 df-dif 3037 df-un 3039 df-in 3041 df-ss 3048 df-nul 3328 df-pw 3476 df-sn 3497 df-pr 3498 df-op 3500 df-uni 3701 df-br 3894 df-opab 3948 df-mpt 3949 df-id 4173 df-suc 4251 df-xp 4503 df-rel 4504 df-cnv 4505 df-co 4506 df-dm 4507 df-rn 4508 df-iota 5044 df-fun 5081 df-fv 5087 df-1st 5990 df-2nd 5991 df-1o 6265 df-dju 6873

This theorem is referenced by: updjudhf 6914

W3C validator