This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )
21 5 20 syl ⊢ ( 𝐾 ∈ 𝐷 → 𝐴 = { 𝑥 ∈ 𝐵 ∣ 0 𝐶 𝑥 } )