Metamath Proof Explorer

Theorem sbthlem2

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

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

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 1 2 sbthlem1 ⊢ ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
4 imass2 ⊢ ( ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝑓 “ ∪ 𝐷 ) ⊆ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
5 sscon ⊢ ( ( 𝑓 “ ∪ 𝐷 ) ⊆ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) → ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ⊆ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) )
6 3 4 5 mp2b ⊢ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ⊆ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) )
7 imass2 ⊢ ( ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ⊆ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
8 sscon ⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ) )
9 6 7 8 mp2b ⊢ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) )
10 imassrn ⊢ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ran 𝑔
11 sstr2 ⊢ ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ran 𝑔 → ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ 𝐴 ) )
12 10 11 ax-mp ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ 𝐴 )
13 difss ⊢ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴
14 ssconb ⊢ ( ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ 𝐴 ∧ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴 ) → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ↔ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ) ) )
15 12 13 14 sylancl ⊢ ( ran 𝑔 ⊆ 𝐴 → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ↔ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ) ) )
16 9 15 mpbiri ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
17 16 13 jctil ⊢ ( ran 𝑔 ⊆ 𝐴 → ( ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) )
18 1 difexi ⊢ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∈ V
19 sseq1 ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴 ) )
20 imaeq2 ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝑓 “ 𝑥 ) = ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
21 20 difeq2d ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) = ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) )
22 21 imaeq2d ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) = ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) )
23 difeq2 ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) )
24 22 23 sseq12d ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ↔ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) )
25 19 24 anbi12d ⊢ ( 𝑥 = ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) ↔ ( ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) )
26 18 25 elab ⊢ ( ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) } ↔ ( ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) ) ⊆ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ) ) )
27 17 26 sylibr ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) } )
28 27 2 eleqtrrdi ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∈ 𝐷 )
29 elssuni ⊢ ( ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ∈ 𝐷 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 )
30 28 29 syl ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ ∪ 𝐷 )