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

Metamath Proof Explorer

Theorem coftr

Description: If there is a cofinal map from B to A and another from C to A , then there is also a cofinal map from C to B . Proposition 11.9 of TakeutiZaring p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof . (Contributed by Mario Carneiro, 16-Mar-2013)

Ref Expression
Hypothesis coftr.1 ⊢ 𝐻 = ( 𝑡 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
Assertion coftr ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 coftr.1 ⊢ 𝐻 = ( 𝑡 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
2 fdm ⊢ ( 𝑔 : 𝐶 ⟶ 𝐴 → dom 𝑔 = 𝐶 )
3 vex ⊢ 𝑔 ∈ V
4 3 dmex ⊢ dom 𝑔 ∈ V
5 2 4 eqeltrrdi ⊢ ( 𝑔 : 𝐶 ⟶ 𝐴 → 𝐶 ∈ V )
6 fveq2 ⊢ ( 𝑡 = 𝑤 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 𝑤 ) )
7 6 sseq1d ⊢ ( 𝑡 = 𝑤 → ( ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) ↔ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) ) )
8 7 rabbidv ⊢ ( 𝑡 = 𝑤 → { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) } = { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
9 8 inteqd ⊢ ( 𝑡 = 𝑤 → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) } = ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
10 9 cbvmptv ⊢ ( 𝑡 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑡 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ) = ( 𝑤 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
11 1 10 eqtri ⊢ 𝐻 = ( 𝑤 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
12 mptexg ⊢ ( 𝐶 ∈ V → ( 𝑤 ∈ 𝐶 ↦ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ) ∈ V )
13 11 12 eqeltrid ⊢ ( 𝐶 ∈ V → 𝐻 ∈ V )
14 5 13 syl ⊢ ( 𝑔 : 𝐶 ⟶ 𝐴 → 𝐻 ∈ V )
15 14 ad2antrl ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → 𝐻 ∈ V )
16 ffn ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝑓 Fn 𝐵 )
17 smodm2 ⊢ ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) → Ord 𝐵 )
18 16 17 sylan ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → Ord 𝐵 )
19 18 3adant3 ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → Ord 𝐵 )
20 19 adantr ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → Ord 𝐵 )
21 simpl3 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) )
22 simprl ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → 𝑔 : 𝐶 ⟶ 𝐴 )
23 simpl1 ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → Ord 𝐵 )
24 simpl2 ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) )
25 ffvelcdm ⊢ ( ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ 𝑤 ∈ 𝐶 ) → ( 𝑔 ‘ 𝑤 ) ∈ 𝐴 )
26 25 3ad2antl3 ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ( 𝑔 ‘ 𝑤 ) ∈ 𝐴 )
27 sseq1 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑤 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
28 27 rexbidv ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑤 ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
29 28 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( ( 𝑔 ‘ 𝑤 ) ∈ 𝐴 → ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
30 24 26 29 sylc ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) )
31 ssrab2 ⊢ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ 𝐵
32 ordsson ⊢ ( Ord 𝐵 → 𝐵 ⊆ On )
33 31 32 sstrid ⊢ ( Ord 𝐵 → { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ On )
34 fveq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑦 ) )
35 34 sseq2d ⊢ ( 𝑛 = 𝑦 → ( ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) ↔ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
36 35 rspcev ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑛 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) )
37 rabn0 ⊢ ( { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ≠ ∅ ↔ ∃ 𝑛 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) )
38 36 37 sylibr ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) → { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ≠ ∅ )
39 oninton ⊢ ( ( { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ On ∧ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ≠ ∅ ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ On )
40 33 38 39 syl2an ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ On )
41 eloni ⊢ ( ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ On → Ord ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
42 40 41 syl ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → Ord ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
43 simpl ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → Ord 𝐵 )
44 35 intminss ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ 𝑦 )
45 44 adantl ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ 𝑦 )
46 simprl ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝐵 )
47 ordtr2 ⊢ ( ( Ord ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∧ Ord 𝐵 ) → ( ( ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ 𝑦 ∧ 𝑦 ∈ 𝐵 ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) )
48 47 imp ⊢ ( ( ( Ord ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∧ Ord 𝐵 ) ∧ ( ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ⊆ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 )
49 42 43 45 46 48 syl22anc ⊢ ( ( Ord 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 )
50 49 rexlimdvaa ⊢ ( Ord 𝐵 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) )
51 23 30 50 sylc ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 )
52 51 11 fmptd ⊢ ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) → 𝐻 : 𝐶 ⟶ 𝐵 )
53 20 21 22 52 syl3anc ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → 𝐻 : 𝐶 ⟶ 𝐵 )
54 simprr ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) )
55 simpl1 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → 𝑓 : 𝐵 ⟶ 𝐴 )
56 ffvelcdm ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝑠 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑠 ) ∈ 𝐴 )
57 sseq1 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑠 ) → ( 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ↔ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
58 57 rexbidv ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑠 ) → ( ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
59 58 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( 𝑓 ‘ 𝑠 ) ∈ 𝐴 → ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
60 56 59 syl5 ⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝑠 ∈ 𝐵 ) → ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
61 60 expdimp ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( 𝑠 ∈ 𝐵 → ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
62 54 55 61 syl2anc ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ( 𝑠 ∈ 𝐵 → ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) )
63 55 16 syl ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → 𝑓 Fn 𝐵 )
64 simpl2 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → Smo 𝑓 )
65 simpr ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → 𝑤 ∈ 𝐶 )
66 65 51 jca ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ( 𝑤 ∈ 𝐶 ∧ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) )
67 35 elrab ⊢ ( 𝑦 ∈ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
68 sstr2 ⊢ ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) → ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
69 smoword ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑠 ⊆ 𝑦 ↔ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) )
70 69 biimprd ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑠 ⊆ 𝑦 ) )
71 68 70 syl9r ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑠 ⊆ 𝑦 ) ) )
72 71 expr ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑠 ⊆ 𝑦 ) ) ) )
73 72 com23 ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑠 ⊆ 𝑦 ) ) ) )
74 73 imp4b ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑦 ) ) → 𝑠 ⊆ 𝑦 ) )
75 67 74 biimtrid ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → ( 𝑦 ∈ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } → 𝑠 ⊆ 𝑦 ) )
76 75 ralrimiv ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → ∀ 𝑦 ∈ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } 𝑠 ⊆ 𝑦 )
77 ssint ⊢ ( 𝑠 ⊆ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ↔ ∀ 𝑦 ∈ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } 𝑠 ⊆ 𝑦 )
78 76 77 sylibr ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → 𝑠 ⊆ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
79 9 1 fvmptg ⊢ ( ( 𝑤 ∈ 𝐶 ∧ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) → ( 𝐻 ‘ 𝑤 ) = ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } )
80 79 sseq2d ⊢ ( ( 𝑤 ∈ 𝐶 ∧ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) → ( 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ↔ 𝑠 ⊆ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ) )
81 78 80 syl5ibrcom ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → ( ( 𝑤 ∈ 𝐶 ∧ ∩ { 𝑛 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑤 ) ⊆ ( 𝑓 ‘ 𝑛 ) } ∈ 𝐵 ) → 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
82 66 81 syl5 ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) ) → ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
83 82 ex ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
84 83 com23 ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) → ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ 𝑤 ∈ 𝐶 ) → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
85 84 expdimp ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ) → ( 𝑤 ∈ 𝐶 → ( ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
86 85 reximdvai ⊢ ( ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ∧ ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ) → ( ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
87 86 ancoms ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ 𝑠 ∈ 𝐵 ) ) → ( ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
88 87 expr ⊢ ( ( ( Ord 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ∧ 𝑔 : 𝐶 ⟶ 𝐴 ) ∧ ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ) → ( 𝑠 ∈ 𝐵 → ( ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
89 20 21 22 63 64 88 syl32anc ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ( 𝑠 ∈ 𝐵 → ( ∃ 𝑤 ∈ 𝐶 ( 𝑓 ‘ 𝑠 ) ⊆ ( 𝑔 ‘ 𝑤 ) → ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
90 62 89 mpdd ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ( 𝑠 ∈ 𝐵 → ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
91 90 ralrimiv ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) )
92 feq1 ⊢ ( ℎ = 𝐻 → ( ℎ : 𝐶 ⟶ 𝐵 ↔ 𝐻 : 𝐶 ⟶ 𝐵 ) )
93 fveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) )
94 93 sseq2d ⊢ ( ℎ = 𝐻 → ( 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ↔ 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
95 94 rexbidv ⊢ ( ℎ = 𝐻 → ( ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ↔ ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
96 95 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ↔ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) )
97 92 96 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ↔ ( 𝐻 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) ) )
98 97 spcegv ⊢ ( 𝐻 ∈ V → ( ( 𝐻 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ) )
99 98 3impib ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( 𝐻 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) )
100 15 53 91 99 syl3anc ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) )
101 100 ex ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ) )
102 101 exlimdv ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ) )
103 102 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝐶 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐶 𝑧 ⊆ ( 𝑔 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : 𝐶 ⟶ 𝐵 ∧ ∀ 𝑠 ∈ 𝐵 ∃ 𝑤 ∈ 𝐶 𝑠 ⊆ ( ℎ ‘ 𝑤 ) ) ) )