Metamath Proof Explorer

Theorem sbthlem9

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

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

Proof

Step Hyp Ref Expression
1 sbthlem.1 ⊢ 𝐴 ∈ V
2 sbthlem.2 ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ( 𝑔 “ ( 𝐵 ∖ ( 𝑓 “ 𝑥 ) ) ) ⊆ ( 𝐴 ∖ 𝑥 ) ) }
3 sbthlem.3 ⊢ 𝐻 = ( ( 𝑓 ↾ ∪ 𝐷 ) ∪ ( ◡ 𝑔 ↾ ( 𝐴 ∖ ∪ 𝐷 ) ) )
4 1 2 3 sbthlem7 ⊢ ( ( Fun 𝑓 ∧ Fun ◡ 𝑔 ) → Fun 𝐻 )
5 1 2 3 sbthlem5 ⊢ ( ( dom 𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴 ) → dom 𝐻 = 𝐴 )
6 5 adantrl ⊢ ( ( dom 𝑓 = 𝐴 ∧ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) → dom 𝐻 = 𝐴 )
7 4 6 anim12i ⊢ ( ( ( Fun 𝑓 ∧ Fun ◡ 𝑔 ) ∧ ( dom 𝑓 = 𝐴 ∧ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) )
8 7 an42s ⊢ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) )
9 8 adantlr ⊢ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) )
10 9 adantlr ⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) )
11 1 2 3 sbthlem8 ⊢ ( ( Fun ◡ 𝑓 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ◡ 𝐻 )
12 11 adantll ⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → Fun ◡ 𝐻 )
13 simpr ⊢ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) → dom 𝑔 = 𝐵 )
14 13 anim1i ⊢ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) → ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) )
15 df-rn ⊢ ran 𝐻 = dom ◡ 𝐻
16 1 2 3 sbthlem6 ⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ran 𝐻 = 𝐵 )
17 15 16 eqtr3id ⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 )
18 14 17 sylanr1 ⊢ ( ( ran 𝑓 ⊆ 𝐵 ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 )
19 18 adantll ⊢ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 )
20 19 adantlr ⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → dom ◡ 𝐻 = 𝐵 )
21 10 12 20 jca32 ⊢ ( ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) → ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) )
22 df-f1 ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) )
23 df-f ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) )
24 df-fn ⊢ ( 𝑓 Fn 𝐴 ↔ ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) )
25 24 anbi1i ⊢ ( ( 𝑓 Fn 𝐴 ∧ ran 𝑓 ⊆ 𝐵 ) ↔ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) )
26 23 25 bitri ⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) )
27 26 anbi1i ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝑓 ) ↔ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) )
28 22 27 bitri ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) )
29 df-f1 ⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 ↔ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑔 ) )
30 df-f ⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( 𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) )
31 df-fn ⊢ ( 𝑔 Fn 𝐵 ↔ ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) )
32 31 anbi1i ⊢ ( ( 𝑔 Fn 𝐵 ∧ ran 𝑔 ⊆ 𝐴 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) )
33 30 32 bitri ⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) )
34 33 anbi1i ⊢ ( ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ Fun ◡ 𝑔 ) ↔ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) )
35 29 34 bitri ⊢ ( 𝑔 : 𝐵 –1-1→ 𝐴 ↔ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) )
36 28 35 anbi12i ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) ↔ ( ( ( ( Fun 𝑓 ∧ dom 𝑓 = 𝐴 ) ∧ ran 𝑓 ⊆ 𝐵 ) ∧ Fun ◡ 𝑓 ) ∧ ( ( ( Fun 𝑔 ∧ dom 𝑔 = 𝐵 ) ∧ ran 𝑔 ⊆ 𝐴 ) ∧ Fun ◡ 𝑔 ) ) )
37 dff1o4 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 Fn 𝐴 ∧ ◡ 𝐻 Fn 𝐵 ) )
38 df-fn ⊢ ( 𝐻 Fn 𝐴 ↔ ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) )
39 df-fn ⊢ ( ◡ 𝐻 Fn 𝐵 ↔ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) )
40 38 39 anbi12i ⊢ ( ( 𝐻 Fn 𝐴 ∧ ◡ 𝐻 Fn 𝐵 ) ↔ ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) )
41 37 40 bitri ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( ( Fun 𝐻 ∧ dom 𝐻 = 𝐴 ) ∧ ( Fun ◡ 𝐻 ∧ dom ◡ 𝐻 = 𝐵 ) ) )
42 21 36 41 3imtr4i ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑔 : 𝐵 –1-1→ 𝐴 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )