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		ffvelrn	⊢ ( ( 𝑔 : ( 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 ‘ 𝐵 ) ) )