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

Metamath Proof Explorer

Theorem sbthlem3

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

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

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 1 2 sbthlem2 ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 )
4 1 2 sbthlem1 ⊢ ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
5 3 4 jctil ⊢ ( ran 𝑔 ⊆ 𝐴 → ( ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∧ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 ) )
6 eqss ⊢ ( ∪ 𝐷 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ↔ ( ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∧ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 ) )
7 5 6 sylibr ⊢ ( ran 𝑔 ⊆ 𝐴 → ∪ 𝐷 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) )
8 7 difeq2d ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ∪ 𝐷 ) = ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
9 imassrn ⊢ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ ran 𝑔
10 sstr2 ⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ ran 𝑔 → ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 ) )
11 9 10 ax-mp ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 )
12 dfss4 ⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) = ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
13 11 12 sylib ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) = ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
14 8 13 eqtr2d ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐴 ∖ ∪ 𝐷 ) )