Theorem pats

Description: The set of atoms in a poset. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	patoms.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	patoms.z	⊢ 0 = ( 0. ‘ 𝐾 )
	patoms.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	patoms.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	pats	⊢ ( 𝐾 ∈ 𝐷 → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		patoms.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		patoms.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		patoms.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		patoms.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		elex	⊢ ( 𝐾 ∈ 𝐷 → 𝐾 ∈ V )
6		fveq2	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
7	6 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
8		fveq2	⊢ ( 𝑝 = 𝐾 → ( ⋖ ‘ 𝑝 ) = ( ⋖ ‘ 𝐾 ) )
9	8 3	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( ⋖ ‘ 𝑝 ) = 𝐶 )
10	9	breqd	⊢ ( 𝑝 = 𝐾 → ( ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑥 ↔ ( 0. ‘ 𝑝 ) 𝐶 𝑥 ) )
11		fveq2	⊢ ( 𝑝 = 𝐾 → ( 0. ‘ 𝑝 ) = ( 0. ‘ 𝐾 ) )
12	11 2	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( 0. ‘ 𝑝 ) = 0 )
13	12	breq1d	⊢ ( 𝑝 = 𝐾 → ( ( 0. ‘ 𝑝 ) 𝐶 𝑥 ↔ 0 𝐶 𝑥 ) )
14	10 13	bitrd	⊢ ( 𝑝 = 𝐾 → ( ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑥 ↔ 0 𝐶 𝑥 ) )
15	7 14	rabeqbidv	⊢ ( 𝑝 = 𝐾 → { 𝑥 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑥 } = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )
16		df-ats	⊢ Atoms = ( 𝑝 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑝 ) ∣ ( 0. ‘ 𝑝 ) ( ⋖ ‘ 𝑝 ) 𝑥 } )
17	1	fvexi	⊢ 𝐵 ∈ V
18	17	rabex	⊢ { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } ∈ V
19	15 16 18	fvmpt	⊢ ( 𝐾 ∈ V → ( Atoms ‘ 𝐾 ) = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )
20	4 19	syl5eq	⊢ ( 𝐾 ∈ V → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )
21	5 20	syl	⊢ ( 𝐾 ∈ 𝐷 → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )