bnj1143

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj1143	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
2		notnotb	⊢ ( 𝐴 = ∅ ↔ ¬ ¬ 𝐴 = ∅ )
3		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
4	2 3	xchbinx	⊢ ( 𝐴 = ∅ ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝐴 )
5		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) )
6		exsimpl	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑥 𝑥 ∈ 𝐴 )
7	5 6	sylbi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → ∃ 𝑥 𝑥 ∈ 𝐴 )
8	7	con3i	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝐴 → ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
9	4 8	sylbi	⊢ ( 𝐴 = ∅ → ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
10	9	alrimiv	⊢ ( 𝐴 = ∅ → ∀ 𝑧 ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
11		notnotb	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ ↔ ¬ ¬ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ )
12		neq0	⊢ ( ¬ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∃ 𝑧 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
13	1	eqeq1i	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ )
14	13	notbii	⊢ ( ¬ ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ¬ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ )
15		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 }
16	15	eleq2i	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } )
17	16	exbii	⊢ ( ∃ 𝑧 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑧 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } )
18	12 14 17	3bitr3i	⊢ ( ¬ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ ↔ ∃ 𝑧 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } )
19	11 18	xchbinx	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ ↔ ¬ ∃ 𝑧 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } )
20		alnex	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ¬ ∃ 𝑧 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } )
21		abid	⊢ ( 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
22	21	notbii	⊢ ( ¬ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
23	22	albii	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ∀ 𝑧 ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
24	19 20 23	3bitr2i	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ ↔ ∀ 𝑧 ¬ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
25	10 24	sylibr	⊢ ( 𝐴 = ∅ → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = ∅ )
26	1 25	eqtrid	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = ∅ )
27		0ss	⊢ ∅ ⊆ 𝐵
28	26 27	eqsstrdi	⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )
29		iunconst	⊢ ( 𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵 )
30		eqimss	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )
31	29 30	syl	⊢ ( 𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵 )
32	28 31	pm2.61ine	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵

Metamath Proof Explorer

Theorem bnj1143

Proof