Metamath Proof Explorer

Theorem cfcoflem

Description: Lemma for cfcof , showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Assertion cfcoflem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cff1 ⊢ ( 𝐵 ∈ On → ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐵 ) –1-1→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) )
2 f1f ⊢ ( 𝑔 : ( cf ‘ 𝐵 ) –1-1→ 𝐵 → 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 )
3 fco ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) : ( cf ‘ 𝐵 ) ⟶ 𝐴 )
4 3 adantlr ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑓 ∘ 𝑔 ) : ( cf ‘ 𝐵 ) ⟶ 𝐴 )
5 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
6 ffvelcdm ⊢ ( ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 )
7 ffn ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝑓 Fn 𝐵 )
8 smoword ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 ) ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ↔ ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
9 8 biimpd ⊢ ( ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 ) ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
10 9 exp32 ⊢ ( ( 𝑓 Fn 𝐵 ∧ Smo 𝑓 ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) ) ) )
11 7 10 sylan ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑔 ‘ 𝑧 ) ∈ 𝐵 → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) ) ) )
12 6 11 syl7 ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → ( 𝑦 ∈ 𝐵 → ( ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) ) ) )
13 12 com23 ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → ( ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) ) ) )
14 13 expdimp ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑧 ∈ ( cf ‘ 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) ) ) )
15 14 3imp2 ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) )
16 sstr2 ⊢ ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( ( 𝑓 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) → 𝑥 ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
17 15 16 syl5com ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑥 ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
18 fvco3 ⊢ ( ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) = ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) )
19 18 sseq2d ⊢ ( ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ↔ 𝑥 ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
20 19 adantll ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ↔ 𝑥 ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
21 20 3ad2antr1 ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ↔ 𝑥 ⊆ ( 𝑓 ‘ ( 𝑔 ‘ 𝑧 ) ) ) )
22 17 21 sylibrd ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
23 22 expcom ⊢ ( ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) → ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) )
24 23 3expia ⊢ ( ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) ) )
25 24 com4t ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) ) )
26 25 imp ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑧 ∈ ( cf ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) )
27 26 expcomd ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ ( cf ‘ 𝐵 ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) ) )
28 27 imp31 ⊢ ( ( ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ ( cf ‘ 𝐵 ) ) → ( 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
29 28 reximdva ⊢ ( ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
30 29 exp31 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( 𝑦 ∈ 𝐵 → ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) ) )
31 30 com34 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) ) )
32 31 impcomd ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) )
33 32 com23 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( 𝑦 ∈ 𝐵 → ( ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) )
34 33 rexlimdv ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
35 5 34 syl5 ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) → ( ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
36 35 expdimp ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
37 36 ralimdv ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
38 37 impr ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) )
39 vex ⊢ 𝑓 ∈ V
40 vex ⊢ 𝑔 ∈ V
41 39 40 coex ⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
42 feq1 ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ↔ ( 𝑓 ∘ 𝑔 ) : ( cf ‘ 𝐵 ) ⟶ 𝐴 ) )
43 fveq1 ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ ‘ 𝑧 ) = ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) )
44 43 sseq2d ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ↔ 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
45 44 rexbidv ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ↔ ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
46 45 ralbidv ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) )
47 42 46 anbi12d ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ↔ ( ( 𝑓 ∘ 𝑔 ) : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) ) )
48 41 47 spcev ⊢ ( ( ( 𝑓 ∘ 𝑔 ) : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑧 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) )
49 4 38 48 syl2an2r ⊢ ( ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) ∧ 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 ) ∧ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) )
50 49 exp43 ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) ) )
51 50 com24 ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) ) )
52 51 3impia ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) )
53 52 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) )
54 53 com13 ⊢ ( 𝑔 : ( cf ‘ 𝐵 ) ⟶ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) )
55 2 54 syl ⊢ ( 𝑔 : ( cf ‘ 𝐵 ) –1-1→ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) ) )
56 55 imp ⊢ ( ( 𝑔 : ( cf ‘ 𝐵 ) –1-1→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) )
57 56 exlimiv ⊢ ( ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐵 ) –1-1→ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑦 ⊆ ( 𝑔 ‘ 𝑧 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) )
58 1 57 syl ⊢ ( 𝐵 ∈ On → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) ) )
59 cfon ⊢ ( cf ‘ 𝐵 ) ∈ On
60 cfflb ⊢ ( ( 𝐴 ∈ On ∧ ( cf ‘ 𝐵 ) ∈ On ) → ( ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) ) )
61 59 60 mpan2 ⊢ ( 𝐴 ∈ On → ( ∃ ℎ ( ℎ : ( cf ‘ 𝐵 ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ( cf ‘ 𝐵 ) 𝑥 ⊆ ( ℎ ‘ 𝑧 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) ) )
62 58 61 sylan9r ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) ) )