Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003)

	Ref	Expression
Hypotheses	cplem1.1	⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
	cplem1.2	⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶
Assertion	cplem1	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) }
2		cplem1.2	⊢ 𝐷 = ∪ 𝑥 ∈ 𝐴 𝐶
3		scott0	⊢ ( 𝐵 = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
4	1	eqeq1i	⊢ ( 𝐶 = ∅ ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑧 ∈ 𝐵 ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑧 ) } = ∅ )
5	3 4	bitr4i	⊢ ( 𝐵 = ∅ ↔ 𝐶 = ∅ )
6	5	necon3bii	⊢ ( 𝐵 ≠ ∅ ↔ 𝐶 ≠ ∅ )
7		n0	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
8	6 7	bitri	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
9	1	ssrab3	⊢ 𝐶 ⊆ 𝐵
10	9	sseli	⊢ ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐵 )
11	10	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐵 ) )
12		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶 )
13	12 2	sseqtrrdi	⊢ ( 𝑥 ∈ 𝐴 → 𝐶 ⊆ 𝐷 )
14	13	sseld	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → 𝑤 ∈ 𝐷 ) )
15	11 14	jcad	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) ) )
16		inelcm	⊢ ( ( 𝑤 ∈ 𝐵 ∧ 𝑤 ∈ 𝐷 ) → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )
17	15 16	syl6	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐶 → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
18	17	exlimdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑤 𝑤 ∈ 𝐶 → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
19	8 18	syl5bi	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ ) )
20	19	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐷 ) ≠ ∅ )