Metamath Proof Explorer

Theorem cofsmo

Description: Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of TakeutiZaring p. 101. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Hypotheses cofsmo.1 ⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) }
cofsmo.2 ⊢ 𝐾 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) }
cofsmo.3 ⊢ 𝑂 = OrdIso ( E , 𝐶 )
Assertion cofsmo ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑥 ∈ suc 𝐵 ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )

Proof

Step Hyp Ref Expression
1 cofsmo.1 ⊢ 𝐶 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) }
2 cofsmo.2 ⊢ 𝐾 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) }
3 cofsmo.3 ⊢ 𝑂 = OrdIso ( E , 𝐶 )
4 1 ssrab3 ⊢ 𝐶 ⊆ 𝐵
5 ssexg ⊢ ( ( 𝐶 ⊆ 𝐵 ∧ 𝐵 ∈ On ) → 𝐶 ∈ V )
6 4 5 mpan ⊢ ( 𝐵 ∈ On → 𝐶 ∈ V )
7 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
8 4 7 sstrid ⊢ ( 𝐵 ∈ On → 𝐶 ⊆ On )
9 epweon ⊢ E We On
10 wess ⊢ ( 𝐶 ⊆ On → ( E We On → E We 𝐶 ) )
11 8 9 10 mpisyl ⊢ ( 𝐵 ∈ On → E We 𝐶 )
12 3 oiiso ⊢ ( ( 𝐶 ∈ V ∧ E We 𝐶 ) → 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) )
13 6 11 12 syl2anc ⊢ ( 𝐵 ∈ On → 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) )
14 13 ad2antlr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) )
15 isof1o ⊢ ( 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) → 𝑂 : dom 𝑂 –1-1-onto→ 𝐶 )
16 f1ofo ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ 𝐶 → 𝑂 : dom 𝑂 –onto→ 𝐶 )
17 14 15 16 3syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑂 : dom 𝑂 –onto→ 𝐶 )
18 fof ⊢ ( 𝑂 : dom 𝑂 –onto→ 𝐶 → 𝑂 : dom 𝑂 ⟶ 𝐶 )
19 fss ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐶 ∧ 𝐶 ⊆ 𝐵 ) → 𝑂 : dom 𝑂 ⟶ 𝐵 )
20 18 4 19 sylancl ⊢ ( 𝑂 : dom 𝑂 –onto→ 𝐶 → 𝑂 : dom 𝑂 ⟶ 𝐵 )
21 17 20 syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑂 : dom 𝑂 ⟶ 𝐵 )
22 3 oion ⊢ ( 𝐶 ∈ V → dom 𝑂 ∈ On )
23 6 22 syl ⊢ ( 𝐵 ∈ On → dom 𝑂 ∈ On )
24 23 ad2antlr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → dom 𝑂 ∈ On )
25 simplr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝐵 ∈ On )
26 eloni ⊢ ( dom 𝑂 ∈ On → Ord dom 𝑂 )
27 smoiso2 ⊢ ( ( Ord dom 𝑂 ∧ 𝐶 ⊆ On ) → ( ( 𝑂 : dom 𝑂 –onto→ 𝐶 ∧ Smo 𝑂 ) ↔ 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) ) )
28 26 8 27 syl2an ⊢ ( ( dom 𝑂 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑂 : dom 𝑂 –onto→ 𝐶 ∧ Smo 𝑂 ) ↔ 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) ) )
29 28 biimpar ⊢ ( ( ( dom 𝑂 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) ) → ( 𝑂 : dom 𝑂 –onto→ 𝐶 ∧ Smo 𝑂 ) )
30 29 simprd ⊢ ( ( ( dom 𝑂 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑂 Isom E , E ( dom 𝑂 , 𝐶 ) ) → Smo 𝑂 )
31 24 25 14 30 syl21anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → Smo 𝑂 )
32 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
33 32 ad2antlr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → Ord 𝐵 )
34 smorndom ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐵 ∧ Smo 𝑂 ∧ Ord 𝐵 ) → dom 𝑂 ⊆ 𝐵 )
35 21 31 33 34 syl3anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → dom 𝑂 ⊆ 𝐵 )
36 onsssuc ⊢ ( ( dom 𝑂 ∈ On ∧ 𝐵 ∈ On ) → ( dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵 ) )
37 24 25 36 syl2anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( dom 𝑂 ⊆ 𝐵 ↔ dom 𝑂 ∈ suc 𝐵 ) )
38 35 37 mpbid ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → dom 𝑂 ∈ suc 𝐵 )
39 38 adantrr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → dom 𝑂 ∈ suc 𝐵 )
40 vex ⊢ 𝑓 ∈ V
41 3 oiexg ⊢ ( 𝐶 ∈ V → 𝑂 ∈ V )
42 6 41 syl ⊢ ( 𝐵 ∈ On → 𝑂 ∈ V )
43 42 ad2antlr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑂 ∈ V )
44 coexg ⊢ ( ( 𝑓 ∈ V ∧ 𝑂 ∈ V ) → ( 𝑓 ∘ 𝑂 ) ∈ V )
45 40 43 44 sylancr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( 𝑓 ∘ 𝑂 ) ∈ V )
46 simprl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑓 : 𝐵 ⟶ 𝐴 )
47 21 adantrr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑂 : dom 𝑂 ⟶ 𝐵 )
48 46 47 fcod ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 )
49 simpr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑓 : 𝐵 ⟶ 𝐴 )
50 49 21 fcod ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 )
51 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
52 51 ad2antrr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝐴 ⊆ On )
53 24 26 syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → Ord dom 𝑂 )
54 17 18 syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑂 : dom 𝑂 ⟶ 𝐶 )
55 simpl ⊢ ( ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) → 𝑠 ∈ dom 𝑂 )
56 ffvelrn ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐶 ∧ 𝑠 ∈ dom 𝑂 ) → ( 𝑂 ‘ 𝑠 ) ∈ 𝐶 )
57 54 55 56 syl2an ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( 𝑂 ‘ 𝑠 ) ∈ 𝐶 )
58 ffn ⊢ ( 𝑂 : dom 𝑂 ⟶ 𝐶 → 𝑂 Fn dom 𝑂 )
59 17 18 58 3syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → 𝑂 Fn dom 𝑂 )
60 59 31 jca ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( 𝑂 Fn dom 𝑂 ∧ Smo 𝑂 ) )
61 smoel2 ⊢ ( ( ( 𝑂 Fn dom 𝑂 ∧ Smo 𝑂 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( 𝑂 ‘ 𝑡 ) ∈ ( 𝑂 ‘ 𝑠 ) )
62 60 61 sylan ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( 𝑂 ‘ 𝑡 ) ∈ ( 𝑂 ‘ 𝑠 ) )
63 fveq2 ⊢ ( 𝑧 = ( 𝑂 ‘ 𝑠 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) )
64 63 eleq2d ⊢ ( 𝑧 = ( 𝑂 ‘ 𝑠 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
65 64 raleqbi1dv ⊢ ( 𝑧 = ( 𝑂 ‘ 𝑠 ) → ( ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ ( 𝑂 ‘ 𝑠 ) ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
66 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑓 ‘ 𝑤 ) = ( 𝑓 ‘ 𝑥 ) )
67 66 eleq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑦 ) ) )
68 67 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑦 ) )
69 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑧 ) )
70 69 eleq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) ) )
71 70 raleqbi1dv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) ) )
72 68 71 syl5bb ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) ) )
73 72 cbvrabv ⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) } = { 𝑧 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) }
74 1 73 eqtri ⊢ 𝐶 = { 𝑧 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑧 ) }
75 65 74 elrab2 ⊢ ( ( 𝑂 ‘ 𝑠 ) ∈ 𝐶 ↔ ( ( 𝑂 ‘ 𝑠 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑂 ‘ 𝑠 ) ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
76 75 simprbi ⊢ ( ( 𝑂 ‘ 𝑠 ) ∈ 𝐶 → ∀ 𝑥 ∈ ( 𝑂 ‘ 𝑠 ) ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) )
77 fveq2 ⊢ ( 𝑥 = ( 𝑂 ‘ 𝑡 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) )
78 77 eleq1d ⊢ ( 𝑥 = ( 𝑂 ‘ 𝑡 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ↔ ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
79 78 rspccv ⊢ ( ∀ 𝑥 ∈ ( 𝑂 ‘ 𝑠 ) ( 𝑓 ‘ 𝑥 ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) → ( ( 𝑂 ‘ 𝑡 ) ∈ ( 𝑂 ‘ 𝑠 ) → ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
80 76 79 syl ⊢ ( ( 𝑂 ‘ 𝑠 ) ∈ 𝐶 → ( ( 𝑂 ‘ 𝑡 ) ∈ ( 𝑂 ‘ 𝑠 ) → ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) ) )
81 57 62 80 sylc ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) ∈ ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) )
82 ordtr1 ⊢ ( Ord dom 𝑂 → ( ( 𝑡 ∈ 𝑠 ∧ 𝑠 ∈ dom 𝑂 ) → 𝑡 ∈ dom 𝑂 ) )
83 82 ancomsd ⊢ ( Ord dom 𝑂 → ( ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) → 𝑡 ∈ dom 𝑂 ) )
84 24 26 83 3syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) → 𝑡 ∈ dom 𝑂 ) )
85 84 imp ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → 𝑡 ∈ dom 𝑂 )
86 fvco3 ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐵 ∧ 𝑡 ∈ dom 𝑂 ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) )
87 21 85 86 syl2an2r ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑡 ) ) )
88 simprl ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → 𝑠 ∈ dom 𝑂 )
89 fvco3 ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐵 ∧ 𝑠 ∈ dom 𝑂 ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) )
90 21 88 89 syl2an2r ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑠 ) ) )
91 81 87 90 3eltr4d ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ( 𝑠 ∈ dom 𝑂 ∧ 𝑡 ∈ 𝑠 ) ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) ∈ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) )
92 91 ralrimivva ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ∀ 𝑠 ∈ dom 𝑂 ∀ 𝑡 ∈ 𝑠 ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) ∈ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) )
93 issmo2 ⊢ ( ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 → ( ( 𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀ 𝑠 ∈ dom 𝑂 ∀ 𝑡 ∈ 𝑠 ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) ∈ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) ) → Smo ( 𝑓 ∘ 𝑂 ) ) )
94 93 imp ⊢ ( ( ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 ∧ ( 𝐴 ⊆ On ∧ Ord dom 𝑂 ∧ ∀ 𝑠 ∈ dom 𝑂 ∀ 𝑡 ∈ 𝑠 ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑡 ) ∈ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑠 ) ) ) → Smo ( 𝑓 ∘ 𝑂 ) )
95 50 52 53 92 94 syl13anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → Smo ( 𝑓 ∘ 𝑂 ) )
96 95 adantrr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → Smo ( 𝑓 ∘ 𝑂 ) )
97 rabn0 ⊢ ( { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
98 ssrab2 ⊢ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ 𝐵
99 98 7 sstrid ⊢ ( 𝐵 ∈ On → { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ On )
100 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑤 ) )
101 100 sseq2d ⊢ ( 𝑥 = 𝑤 → ( 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
102 101 cbvrabv ⊢ { 𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) } = { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) }
103 102 inteqi ⊢ ∩ { 𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) } = ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) }
104 2 103 eqtri ⊢ 𝐾 = ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) }
105 onint ⊢ ( ( { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ On ∧ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ≠ ∅ ) → ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
106 104 105 eqeltrid ⊢ ( ( { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ On ∧ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ≠ ∅ ) → 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
107 99 106 sylan ⊢ ( ( 𝐵 ∈ On ∧ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ≠ ∅ ) → 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
108 97 107 sylan2br ⊢ ( ( 𝐵 ∈ On ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
109 fveq2 ⊢ ( 𝑤 = 𝐾 → ( 𝑓 ‘ 𝑤 ) = ( 𝑓 ‘ 𝐾 ) )
110 109 sseq2d ⊢ ( 𝑤 = 𝐾 → ( 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) )
111 110 elrab ⊢ ( 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ↔ ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) )
112 108 111 sylib ⊢ ( ( 𝐵 ∈ On ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) )
113 112 ex ⊢ ( 𝐵 ∈ On → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) )
114 113 adantl ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) )
115 simpr2 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) → 𝐾 ∈ 𝐵 )
116 simp3 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝑤 ∈ 𝐾 )
117 104 eleq2i ⊢ ( 𝑤 ∈ 𝐾 ↔ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
118 simp21 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝑓 : 𝐵 ⟶ 𝐴 )
119 simp1l ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → Ord 𝐴 )
120 119 51 syl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐴 ⊆ On )
121 118 120 fssd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝑓 : 𝐵 ⟶ On )
122 simp22 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐾 ∈ 𝐵 )
123 121 122 ffvelrnd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑓 ‘ 𝐾 ) ∈ On )
124 simp1r ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝐵 ∈ On )
125 ontr1 ⊢ ( 𝐵 ∈ On → ( ( 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 ) )
126 125 3impib ⊢ ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) → 𝑤 ∈ 𝐵 )
127 124 116 122 126 syl3anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝑤 ∈ 𝐵 )
128 121 127 ffvelrnd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑓 ‘ 𝑤 ) ∈ On )
129 ontri1 ⊢ ( ( ( 𝑓 ‘ 𝐾 ) ∈ On ∧ ( 𝑓 ‘ 𝑤 ) ∈ On ) → ( ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ↔ ¬ ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
130 123 128 129 syl2anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ↔ ¬ ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
131 simp23 ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) )
132 simpl1 ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝐵 ∈ On )
133 132 99 syl ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ On )
134 sstr ⊢ ( ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) → 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) )
135 126 134 anim12i ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( 𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
136 rabid ⊢ ( 𝑤 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
137 135 136 sylibr ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → 𝑤 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
138 onnmin ⊢ ( ( { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ⊆ On ∧ 𝑤 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) → ¬ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
139 133 137 138 syl2anc ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ∧ ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ¬ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } )
140 139 expr ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑤 ∈ 𝐾 ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) → ( ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) → ¬ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) )
141 124 116 122 131 140 syl31anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑓 ‘ 𝐾 ) ⊆ ( 𝑓 ‘ 𝑤 ) → ¬ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) )
142 130 141 sylbird ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ¬ ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) → ¬ 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) )
143 142 con4d ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑤 ∈ ∩ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } → ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
144 117 143 syl5bi ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑤 ∈ 𝐾 → ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
145 116 144 mpd ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) )
146 145 3expia ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) → ( 𝑤 ∈ 𝐾 → ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
147 146 ralrimiv ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) → ∀ 𝑤 ∈ 𝐾 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) )
148 fveq2 ⊢ ( 𝑦 = 𝐾 → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ 𝐾 ) )
149 148 eleq2d ⊢ ( 𝑦 = 𝐾 → ( ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
150 149 raleqbi1dv ⊢ ( 𝑦 = 𝐾 → ( ∀ 𝑤 ∈ 𝑦 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐾 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
151 150 1 elrab2 ⊢ ( 𝐾 ∈ 𝐶 ↔ ( 𝐾 ∈ 𝐵 ∧ ∀ 𝑤 ∈ 𝐾 ( 𝑓 ‘ 𝑤 ) ∈ ( 𝑓 ‘ 𝐾 ) ) )
152 115 147 151 sylanbrc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) ) → 𝐾 ∈ 𝐶 )
153 152 expcom ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) → ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → 𝐾 ∈ 𝐶 ) )
154 153 3expib ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → ( ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) → ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → 𝐾 ∈ 𝐶 ) ) )
155 154 com13 ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ( 𝐾 ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝐾 ) ) → ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝐾 ∈ 𝐶 ) ) )
156 114 155 syld ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝐾 ∈ 𝐶 ) ) )
157 156 com23 ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( 𝑓 : 𝐵 ⟶ 𝐴 → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → 𝐾 ∈ 𝐶 ) ) )
158 157 imp31 ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → 𝐾 ∈ 𝐶 )
159 foelrn ⊢ ( ( 𝑂 : dom 𝑂 –onto→ 𝐶 ∧ 𝐾 ∈ 𝐶 ) → ∃ 𝑣 ∈ dom 𝑂 𝐾 = ( 𝑂 ‘ 𝑣 ) )
160 17 158 159 syl2an2r ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑣 ∈ dom 𝑂 𝐾 = ( 𝑂 ‘ 𝑣 ) )
161 eleq1 ⊢ ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → ( 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ↔ ( 𝑂 ‘ 𝑣 ) ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) )
162 161 biimpcd ⊢ ( 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } → ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → ( 𝑂 ‘ 𝑣 ) ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ) )
163 fveq2 ⊢ ( 𝑥 = ( 𝑂 ‘ 𝑣 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) )
164 163 sseq2d ⊢ ( 𝑥 = ( 𝑂 ‘ 𝑣 ) → ( 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) ↔ 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
165 66 sseq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) ) )
166 165 cbvrabv ⊢ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } = { 𝑥 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑥 ) }
167 164 166 elrab2 ⊢ ( ( 𝑂 ‘ 𝑣 ) ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } ↔ ( ( 𝑂 ‘ 𝑣 ) ∈ 𝐵 ∧ 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
168 167 simprbi ⊢ ( ( 𝑂 ‘ 𝑣 ) ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } → 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) )
169 162 168 syl6 ⊢ ( 𝐾 ∈ { 𝑤 ∈ 𝐵 ∣ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) } → ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
170 108 169 syl ⊢ ( ( 𝐵 ∈ On ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
171 170 ad5ant24 ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ∧ 𝑣 ∈ dom 𝑂 ) → ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
172 21 ad2antrr ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ∧ 𝑣 ∈ dom 𝑂 ) → 𝑂 : dom 𝑂 ⟶ 𝐵 )
173 fvco3 ⊢ ( ( 𝑂 : dom 𝑂 ⟶ 𝐵 ∧ 𝑣 ∈ dom 𝑂 ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) )
174 172 173 sylancom ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ∧ 𝑣 ∈ dom 𝑂 ) → ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) = ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) )
175 174 sseq2d ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ∧ 𝑣 ∈ dom 𝑂 ) → ( 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ↔ 𝑧 ⊆ ( 𝑓 ‘ ( 𝑂 ‘ 𝑣 ) ) ) )
176 171 175 sylibrd ⊢ ( ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ∧ 𝑣 ∈ dom 𝑂 ) → ( 𝐾 = ( 𝑂 ‘ 𝑣 ) → 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
177 176 reximdva ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ∃ 𝑣 ∈ dom 𝑂 𝐾 = ( 𝑂 ‘ 𝑣 ) → ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
178 160 177 mpd ⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) ∧ ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) )
179 178 ex ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
180 179 ralimdv ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
181 180 impr ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) )
182 48 96 181 3jca ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 ∧ Smo ( 𝑓 ∘ 𝑂 ) ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
183 feq1 ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( 𝑔 : dom 𝑂 ⟶ 𝐴 ↔ ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 ) )
184 smoeq ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( Smo 𝑔 ↔ Smo ( 𝑓 ∘ 𝑂 ) ) )
185 fveq1 ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( 𝑔 ‘ 𝑣 ) = ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) )
186 185 sseq2d ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ↔ 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
187 186 rexbidv ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ↔ ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
188 187 ralbidv ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) )
189 183 184 188 3anbi123d ⊢ ( 𝑔 = ( 𝑓 ∘ 𝑂 ) → ( ( 𝑔 : dom 𝑂 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ↔ ( ( 𝑓 ∘ 𝑂 ) : dom 𝑂 ⟶ 𝐴 ∧ Smo ( 𝑓 ∘ 𝑂 ) ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( ( 𝑓 ∘ 𝑂 ) ‘ 𝑣 ) ) ) )
190 45 182 189 spcedv ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∃ 𝑔 ( 𝑔 : dom 𝑂 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
191 feq2 ⊢ ( 𝑥 = dom 𝑂 → ( 𝑔 : 𝑥 ⟶ 𝐴 ↔ 𝑔 : dom 𝑂 ⟶ 𝐴 ) )
192 rexeq ⊢ ( 𝑥 = dom 𝑂 → ( ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ↔ ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
193 192 ralbidv ⊢ ( 𝑥 = dom 𝑂 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
194 191 193 3anbi13d ⊢ ( 𝑥 = dom 𝑂 → ( ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ↔ ( 𝑔 : dom 𝑂 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )
195 194 exbidv ⊢ ( 𝑥 = dom 𝑂 → ( ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ↔ ∃ 𝑔 ( 𝑔 : dom 𝑂 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )
196 195 rspcev ⊢ ( ( dom 𝑂 ∈ suc 𝐵 ∧ ∃ 𝑔 ( 𝑔 : dom 𝑂 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ dom 𝑂 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) → ∃ 𝑥 ∈ suc 𝐵 ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
197 39 190 196 syl2anc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ∃ 𝑥 ∈ suc 𝐵 ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) )
198 197 ex ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑥 ∈ suc 𝐵 ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )
199 198 exlimdv ⊢ ( ( Ord 𝐴 ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑥 ∈ suc 𝐵 ∃ 𝑔 ( 𝑔 : 𝑥 ⟶ 𝐴 ∧ Smo 𝑔 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑣 ∈ 𝑥 𝑧 ⊆ ( 𝑔 ‘ 𝑣 ) ) ) )