Theorem sstskm

Description: Being a part of ( tarskiMapA ) . (Contributed by FL, 17-Apr-2011) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	sstskm	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ ( tarskiMap ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tskmval	⊢ ( 𝐴 ∈ 𝑉 → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } )
2		df-rab	⊢ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) }
3	2	inteqi	⊢ ∩ { 𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) }
4	1 3	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( tarskiMap ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) } )
5	4	sseq2d	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ ( tarskiMap ‘ 𝐴 ) ↔ 𝐵 ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) } ) )
6		impexp	⊢ ( ( ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) → 𝐵 ⊆ 𝑥 ) ↔ ( 𝑥 ∈ Tarski → ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ) )
7	6	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) → 𝐵 ⊆ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ Tarski → ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ) )
8		ssintab	⊢ ( 𝐵 ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) → 𝐵 ⊆ 𝑥 ) )
9		df-ral	⊢ ( ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ Tarski → ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ) )
10	7 8 9	3bitr4i	⊢ ( 𝐵 ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ Tarski ∧ 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) )
11	5 10	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ⊆ ( tarskiMap ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ Tarski ( 𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥 ) ) )