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 ⊢ ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )