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 ffvelrn ( ( 𝑔 : 𝐶𝐴𝑤𝐶 ) → ( 𝑔𝑤 ) ∈ 𝐴 )
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 ffvelrn ( ( 𝑓 : 𝐵𝐴𝑠𝐵 ) → ( 𝑓𝑠 ) ∈ 𝐴 )
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 syl5bi ( ( ( ( 𝑓 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 𝑓 ∧ ∀ 𝑥𝐴𝑦𝐵 𝑥 ⊆ ( 𝑓𝑦 ) ) → ( ∃ 𝑔 ( 𝑔 : 𝐶𝐴 ∧ ∀ 𝑧𝐴𝑤𝐶 𝑧 ⊆ ( 𝑔𝑤 ) ) → ∃ ( : 𝐶𝐵 ∧ ∀ 𝑠𝐵𝑤𝐶 𝑠 ⊆ ( 𝑤 ) ) ) )