Theorem cplem1

Description: Lemma for the Collection Principle cp . (Contributed by NM, 17-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

	Ref	Expression
Hypothesis	cplem1.1	⊢ 𝐶 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵
Assertion	cplem1	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		cplem1.1	⊢ 𝐶 = ∪ 𝑥 ∈ 𝐴 Scott 𝐵
2		scott0b	⊢ ( 𝐵 = ∅ ↔ Scott 𝐵 = ∅ )
3	2	necon3bii	⊢ ( 𝐵 ≠ ∅ ↔ Scott 𝐵 ≠ ∅ )
4		n0	⊢ ( Scott 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ Scott 𝐵 )
5	3 4	bitri	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ Scott 𝐵 )
6		scottss	⊢ Scott 𝐵 ⊆ 𝐵
7	6	sseli	⊢ ( 𝑦 ∈ Scott 𝐵 → 𝑦 ∈ 𝐵 )
8	7	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ Scott 𝐵 → 𝑦 ∈ 𝐵 ) )
9		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → Scott 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 Scott 𝐵 )
10	9 1	sseqtrrdi	⊢ ( 𝑥 ∈ 𝐴 → Scott 𝐵 ⊆ 𝐶 )
11	10	sseld	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ Scott 𝐵 → 𝑦 ∈ 𝐶 ) )
12	8 11	jcad	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ Scott 𝐵 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
13		inelcm	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
14	12 13	syl6	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ Scott 𝐵 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
15	14	exlimdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 𝑦 ∈ Scott 𝐵 → ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
16	5 15	biimtrid	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐶 ) ≠ ∅ ) )
17	16	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ≠ ∅ → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )