Metamath Proof Explorer

Theorem elkgen

Description: Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Assertion elkgen ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( 𝐴 ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 kgenval ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( π‘˜Gen β€˜ 𝐽 ) = { π‘₯ ∈ 𝒫 𝑋 ∣ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) } )
2 1 eleq2d ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( 𝐴 ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ 𝐴 ∈ { π‘₯ ∈ 𝒫 𝑋 ∣ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) } ) )
3 ineq1 ⊒ ( π‘₯ = 𝐴 β†’ ( π‘₯ ∩ π‘˜ ) = ( 𝐴 ∩ π‘˜ ) )
4 3 eleq1d ⊒ ( π‘₯ = 𝐴 β†’ ( ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ↔ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) )
5 4 imbi2d ⊒ ( π‘₯ = 𝐴 β†’ ( ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ↔ ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
6 5 ralbidv ⊒ ( π‘₯ = 𝐴 β†’ ( βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ↔ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
7 6 elrab ⊒ ( 𝐴 ∈ { π‘₯ ∈ 𝒫 𝑋 ∣ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) } ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) )
8 toponmax ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ 𝑋 ∈ 𝐽 )
9 elpw2g ⊒ ( 𝑋 ∈ 𝐽 β†’ ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 βŠ† 𝑋 ) )
10 8 9 syl ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 βŠ† 𝑋 ) )
11 10 anbi1d ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( ( 𝐴 ∈ 𝒫 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )
12 7 11 bitrid ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( 𝐴 ∈ { π‘₯ ∈ 𝒫 𝑋 ∣ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( π‘₯ ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) } ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )
13 2 12 bitrd ⊒ ( 𝐽 ∈ ( TopOn β€˜ 𝑋 ) β†’ ( 𝐴 ∈ ( π‘˜Gen β€˜ 𝐽 ) ↔ ( 𝐴 βŠ† 𝑋 ∧ βˆ€ π‘˜ ∈ 𝒫 𝑋 ( ( 𝐽 β†Ύt π‘˜ ) ∈ Comp β†’ ( 𝐴 ∩ π‘˜ ) ∈ ( 𝐽 β†Ύt π‘˜ ) ) ) ) )