# Metamath Proof Explorer

## Theorem sbthlem1

Description: Lemma for sbth . (Contributed by NM, 22-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 𝐴 ∈ V
sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
Assertion sbthlem1 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) )

### Proof

Step Hyp Ref Expression
1 sbthlem.1 𝐴 ∈ V
2 sbthlem.2 𝐷 = { 𝑥 ∣ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) }
3 unissb ( 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ) ↔ ∀ 𝑥𝐷 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ) )
4 2 abeq2i ( 𝑥𝐷 ↔ ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) )
5 difss2 ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ 𝐴 )
6 ssconb ( ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ 𝐴 ) → ( 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ↔ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) )
7 6 exbiri ( 𝑥𝐴 → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ 𝐴 → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) → 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ) ) )
8 5 7 syl5 ( 𝑥𝐴 → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) → 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ) ) )
9 8 pm2.43d ( 𝑥𝐴 → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) → 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ) )
10 9 imp ( ( 𝑥𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ⊆ ( 𝐴𝑥 ) ) → 𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) )
11 4 10 sylbi ( 𝑥𝐷𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) )
12 elssuni ( 𝑥𝐷𝑥 𝐷 )
13 imass2 ( 𝑥 𝐷 → ( 𝑓𝑥 ) ⊆ ( 𝑓 𝐷 ) )
14 sscon ( ( 𝑓𝑥 ) ⊆ ( 𝑓 𝐷 ) → ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ⊆ ( 𝐵 ∖ ( 𝑓𝑥 ) ) )
15 12 13 14 3syl ( 𝑥𝐷 → ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ⊆ ( 𝐵 ∖ ( 𝑓𝑥 ) ) )
16 imass2 ( ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ⊆ ( 𝐵 ∖ ( 𝑓𝑥 ) ) → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ⊆ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) )
17 sscon ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ⊆ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ) )
18 15 16 17 3syl ( 𝑥𝐷 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓𝑥 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ) )
19 11 18 sstrd ( 𝑥𝐷𝑥 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) ) )
20 3 19 mprgbir 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 𝐷 ) ) ) )