Metamath Proof Explorer

Theorem sbthlem5

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

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

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 sbthlem.3 ⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
4 3 dmeqi ⊢ dom 𝐻 = dom ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
5 dmun ⊢ dom ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( dom ( 𝑓 ↾ ∪ 𝐷 ) ∪ dom ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
6 dmres ⊢ dom ( 𝑓 ↾ ∪ 𝐷 ) = ( ∪ 𝐷 ∩ dom 𝑓 )
7 dmres ⊢ dom ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ dom ◡ 𝑔 )
8 df-rn ⊢ ran 𝑔 = dom ◡ 𝑔
9 8 eqcomi ⊢ dom ◡ 𝑔 = ran 𝑔
10 9 ineq2i ⊢ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ dom ◡ 𝑔 ) = ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 )
11 7 10 eqtri ⊢ dom ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 )
12 6 11 uneq12i ⊢ ( dom ( 𝑓 ↾ ∪ 𝐷 ) ∪ dom ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) )
13 5 12 eqtri ⊢ dom ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) ) = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) )
14 4 13 eqtri ⊢ dom 𝐻 = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) )
15 1 2 sbthlem1 ⊢ ∪ 𝐷 ⊆ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) )
16 difss ⊢ ( 𝐴 ∖ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ) ⊆ 𝐴
17 15 16 sstri ⊢ ∪ 𝐷 ⊆ 𝐴
18 sseq2 ⊢ ( dom 𝑓 = 𝐴 → ( ∪ 𝐷 ⊆ dom 𝑓 ↔ ∪ 𝐷 ⊆ 𝐴 ) )
19 17 18 mpbiri ⊢ ( dom 𝑓 = 𝐴 → ∪ 𝐷 ⊆ dom 𝑓 )
20 dfss ⊢ ( ∪ 𝐷 ⊆ dom 𝑓 ↔ ∪ 𝐷 = ( ∪ 𝐷 ∩ dom 𝑓 ) )
21 19 20 sylib ⊢ ( dom 𝑓 = 𝐴 → ∪ 𝐷 = ( ∪ 𝐷 ∩ dom 𝑓 ) )
22 21 uneq1d ⊢ ( dom 𝑓 = 𝐴 → ( ∪ 𝐷 ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) )
23 1 2 sbthlem3 ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) = ( 𝐴 ∖ ∪ 𝐷 ) )
24 imassrn ⊢ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ ∪ 𝐷 ) ) ) ⊆ ran 𝑔
25 23 24 eqsstrrdi ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ∪ 𝐷 ) ⊆ ran 𝑔 )
26 dfss ⊢ ( ( 𝐴 ∖ ∪ 𝐷 ) ⊆ ran 𝑔 ↔ ( 𝐴 ∖ ∪ 𝐷 ) = ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) )
27 25 26 sylib ⊢ ( ran 𝑔 ⊆ 𝐴 → ( 𝐴 ∖ ∪ 𝐷 ) = ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) )
28 27 uneq2d ⊢ ( ran 𝑔 ⊆ 𝐴 → ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) ) )
29 22 28 sylan9eq ⊢ ( ( dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴 ) → ( ∪ 𝐷 ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) = ( ( ∪ 𝐷 ∩ dom 𝑓 ) ∪ ( ( 𝐴 ∖ ∪ 𝐷 ) ∩ ran 𝑔 ) ) )
30 14 29 eqtr4id ⊢ ( ( dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴 ) → dom 𝐻 = ( ∪ 𝐷 ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) )
31 undif ⊢ ( ∪ 𝐷 ⊆ 𝐴 ↔ ( ∪ 𝐷 ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) = 𝐴 )
32 17 31 mpbi ⊢ ( ∪ 𝐷 ∪ ( 𝐴 ∖ ∪ 𝐷 ) ) = 𝐴
33 30 32 eqtrdi ⊢ ( ( dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴 ) → dom 𝐻 = 𝐴 )