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𝐵 )