MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coftr Structured version   Visualization version   GIF version

Theorem coftr 9892
Description: If there is a cofinal map from 𝐵 to 𝐴 and another from 𝐶 to 𝐴, then there is also a cofinal map from 𝐶 to 𝐵. Proposition 11.9 of [TakeutiZaring] p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof 9893. (Contributed by Mario Carneiro, 16-Mar-2013.)
Hypothesis
Ref Expression
coftr.1 𝐻 = (𝑡𝐶 {𝑛𝐵 ∣ (𝑔𝑡) ⊆ (𝑓𝑛)})
Assertion
Ref Expression
coftr (∃𝑓(𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) → (∃𝑔(𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤))))
Distinct variable groups:   𝐴,𝑓,𝑔,𝑠,𝑤,𝑥   𝑧,𝐴,𝑓,𝑔,𝑠,𝑤   𝐵,𝑓,𝑔,,𝑠,𝑤   𝐵,𝑛,𝑡,𝑓,𝑔,𝑤   𝑥,𝐵,𝑦,𝑓,𝑔,𝑠,𝑤   𝐶,𝑓,𝑔,,𝑠,𝑤   𝑡,𝐶   𝑧,𝐶   ,𝐻,𝑠,𝑤   𝑦,𝑛
Allowed substitution hints:   𝐴(𝑦,𝑡,,𝑛)   𝐵(𝑧)   𝐶(𝑥,𝑦,𝑛)   𝐻(𝑥,𝑦,𝑧,𝑡,𝑓,𝑔,𝑛)

Proof of Theorem coftr
StepHypRef Expression
1 fdm 6559 . . . . . . . 8 (𝑔:𝐶𝐴 → dom 𝑔 = 𝐶)
2 vex 3417 . . . . . . . . 9 𝑔 ∈ V
32dmex 7694 . . . . . . . 8 dom 𝑔 ∈ V
41, 3eqeltrrdi 2847 . . . . . . 7 (𝑔:𝐶𝐴𝐶 ∈ V)
5 coftr.1 . . . . . . . . 9 𝐻 = (𝑡𝐶 {𝑛𝐵 ∣ (𝑔𝑡) ⊆ (𝑓𝑛)})
6 fveq2 6722 . . . . . . . . . . . . 13 (𝑡 = 𝑤 → (𝑔𝑡) = (𝑔𝑤))
76sseq1d 3937 . . . . . . . . . . . 12 (𝑡 = 𝑤 → ((𝑔𝑡) ⊆ (𝑓𝑛) ↔ (𝑔𝑤) ⊆ (𝑓𝑛)))
87rabbidv 3395 . . . . . . . . . . 11 (𝑡 = 𝑤 → {𝑛𝐵 ∣ (𝑔𝑡) ⊆ (𝑓𝑛)} = {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
98inteqd 4869 . . . . . . . . . 10 (𝑡 = 𝑤 {𝑛𝐵 ∣ (𝑔𝑡) ⊆ (𝑓𝑛)} = {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
109cbvmptv 5163 . . . . . . . . 9 (𝑡𝐶 {𝑛𝐵 ∣ (𝑔𝑡) ⊆ (𝑓𝑛)}) = (𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
115, 10eqtri 2765 . . . . . . . 8 𝐻 = (𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
12 mptexg 7042 . . . . . . . 8 (𝐶 ∈ V → (𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)}) ∈ V)
1311, 12eqeltrid 2842 . . . . . . 7 (𝐶 ∈ V → 𝐻 ∈ V)
144, 13syl 17 . . . . . 6 (𝑔:𝐶𝐴𝐻 ∈ V)
1514ad2antrl 728 . . . . 5 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → 𝐻 ∈ V)
16 ffn 6550 . . . . . . . . 9 (𝑓:𝐵𝐴𝑓 Fn 𝐵)
17 smodm2 8097 . . . . . . . . 9 ((𝑓 Fn 𝐵 ∧ Smo 𝑓) → Ord 𝐵)
1816, 17sylan 583 . . . . . . . 8 ((𝑓:𝐵𝐴 ∧ Smo 𝑓) → Ord 𝐵)
19183adant3 1134 . . . . . . 7 ((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) → Ord 𝐵)
2019adantr 484 . . . . . 6 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → Ord 𝐵)
21 simpl3 1195 . . . . . 6 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦))
22 simprl 771 . . . . . 6 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → 𝑔:𝐶𝐴)
23 simpl1 1193 . . . . . . . 8 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → Ord 𝐵)
24 simpl2 1194 . . . . . . . . 9 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦))
25 ffvelrn 6907 . . . . . . . . . 10 ((𝑔:𝐶𝐴𝑤𝐶) → (𝑔𝑤) ∈ 𝐴)
26253ad2antl3 1189 . . . . . . . . 9 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → (𝑔𝑤) ∈ 𝐴)
27 sseq1 3931 . . . . . . . . . . 11 (𝑥 = (𝑔𝑤) → (𝑥 ⊆ (𝑓𝑦) ↔ (𝑔𝑤) ⊆ (𝑓𝑦)))
2827rexbidv 3221 . . . . . . . . . 10 (𝑥 = (𝑔𝑤) → (∃𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ↔ ∃𝑦𝐵 (𝑔𝑤) ⊆ (𝑓𝑦)))
2928rspccv 3539 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) → ((𝑔𝑤) ∈ 𝐴 → ∃𝑦𝐵 (𝑔𝑤) ⊆ (𝑓𝑦)))
3024, 26, 29sylc 65 . . . . . . . 8 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → ∃𝑦𝐵 (𝑔𝑤) ⊆ (𝑓𝑦))
31 ssrab2 3998 . . . . . . . . . . . . 13 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ 𝐵
32 ordsson 7572 . . . . . . . . . . . . 13 (Ord 𝐵𝐵 ⊆ On)
3331, 32sstrid 3917 . . . . . . . . . . . 12 (Ord 𝐵 → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ On)
34 fveq2 6722 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (𝑓𝑛) = (𝑓𝑦))
3534sseq2d 3938 . . . . . . . . . . . . . 14 (𝑛 = 𝑦 → ((𝑔𝑤) ⊆ (𝑓𝑛) ↔ (𝑔𝑤) ⊆ (𝑓𝑦)))
3635rspcev 3542 . . . . . . . . . . . . 13 ((𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦)) → ∃𝑛𝐵 (𝑔𝑤) ⊆ (𝑓𝑛))
37 rabn0 4305 . . . . . . . . . . . . 13 ({𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ≠ ∅ ↔ ∃𝑛𝐵 (𝑔𝑤) ⊆ (𝑓𝑛))
3836, 37sylibr 237 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦)) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ≠ ∅)
39 oninton 7584 . . . . . . . . . . . 12 (({𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ On ∧ {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ≠ ∅) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ On)
4033, 38, 39syl2an 599 . . . . . . . . . . 11 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ On)
41 eloni 6228 . . . . . . . . . . 11 ( {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ On → Ord {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
4240, 41syl 17 . . . . . . . . . 10 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → Ord {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
43 simpl 486 . . . . . . . . . 10 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → Ord 𝐵)
4435intminss 4890 . . . . . . . . . . 11 ((𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦)) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ 𝑦)
4544adantl 485 . . . . . . . . . 10 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ 𝑦)
46 simprl 771 . . . . . . . . . 10 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → 𝑦𝐵)
47 ordtr2 6262 . . . . . . . . . . 11 ((Ord {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∧ Ord 𝐵) → (( {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ 𝑦𝑦𝐵) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵))
4847imp 410 . . . . . . . . . 10 (((Ord {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∧ Ord 𝐵) ∧ ( {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ⊆ 𝑦𝑦𝐵)) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵)
4942, 43, 45, 46, 48syl22anc 839 . . . . . . . . 9 ((Ord 𝐵 ∧ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦))) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵)
5049rexlimdvaa 3209 . . . . . . . 8 (Ord 𝐵 → (∃𝑦𝐵 (𝑔𝑤) ⊆ (𝑓𝑦) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵))
5123, 30, 50sylc 65 . . . . . . 7 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵)
5251, 11fmptd 6936 . . . . . 6 ((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) → 𝐻:𝐶𝐵)
5320, 21, 22, 52syl3anc 1373 . . . . 5 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → 𝐻:𝐶𝐵)
54 simprr 773 . . . . . . . 8 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))
55 simpl1 1193 . . . . . . . 8 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → 𝑓:𝐵𝐴)
56 ffvelrn 6907 . . . . . . . . . 10 ((𝑓:𝐵𝐴𝑠𝐵) → (𝑓𝑠) ∈ 𝐴)
57 sseq1 3931 . . . . . . . . . . . 12 (𝑧 = (𝑓𝑠) → (𝑧 ⊆ (𝑔𝑤) ↔ (𝑓𝑠) ⊆ (𝑔𝑤)))
5857rexbidv 3221 . . . . . . . . . . 11 (𝑧 = (𝑓𝑠) → (∃𝑤𝐶 𝑧 ⊆ (𝑔𝑤) ↔ ∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤)))
5958rspccv 3539 . . . . . . . . . 10 (∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤) → ((𝑓𝑠) ∈ 𝐴 → ∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤)))
6056, 59syl5 34 . . . . . . . . 9 (∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤) → ((𝑓:𝐵𝐴𝑠𝐵) → ∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤)))
6160expdimp 456 . . . . . . . 8 ((∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤) ∧ 𝑓:𝐵𝐴) → (𝑠𝐵 → ∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤)))
6254, 55, 61syl2anc 587 . . . . . . 7 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → (𝑠𝐵 → ∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤)))
6355, 16syl 17 . . . . . . . 8 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → 𝑓 Fn 𝐵)
64 simpl2 1194 . . . . . . . 8 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → Smo 𝑓)
65 simpr 488 . . . . . . . . . . . . . . . 16 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → 𝑤𝐶)
6665, 51jca 515 . . . . . . . . . . . . . . 15 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → (𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵))
6735elrab 3607 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ↔ (𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦)))
68 sstr2 3913 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑓𝑠) ⊆ (𝑔𝑤) → ((𝑔𝑤) ⊆ (𝑓𝑦) → (𝑓𝑠) ⊆ (𝑓𝑦)))
69 smoword 8108 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ (𝑠𝐵𝑦𝐵)) → (𝑠𝑦 ↔ (𝑓𝑠) ⊆ (𝑓𝑦)))
7069biimprd 251 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ (𝑠𝐵𝑦𝐵)) → ((𝑓𝑠) ⊆ (𝑓𝑦) → 𝑠𝑦))
7168, 70syl9r 78 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ (𝑠𝐵𝑦𝐵)) → ((𝑓𝑠) ⊆ (𝑔𝑤) → ((𝑔𝑤) ⊆ (𝑓𝑦) → 𝑠𝑦)))
7271expr 460 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) → (𝑦𝐵 → ((𝑓𝑠) ⊆ (𝑔𝑤) → ((𝑔𝑤) ⊆ (𝑓𝑦) → 𝑠𝑦))))
7372com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) → ((𝑓𝑠) ⊆ (𝑔𝑤) → (𝑦𝐵 → ((𝑔𝑤) ⊆ (𝑓𝑦) → 𝑠𝑦))))
7473imp4b 425 . . . . . . . . . . . . . . . . . . 19 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → ((𝑦𝐵 ∧ (𝑔𝑤) ⊆ (𝑓𝑦)) → 𝑠𝑦))
7567, 74syl5bi 245 . . . . . . . . . . . . . . . . . 18 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → (𝑦 ∈ {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} → 𝑠𝑦))
7675ralrimiv 3104 . . . . . . . . . . . . . . . . 17 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → ∀𝑦 ∈ {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)}𝑠𝑦)
77 ssint 4880 . . . . . . . . . . . . . . . . 17 (𝑠 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ↔ ∀𝑦 ∈ {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)}𝑠𝑦)
7876, 77sylibr 237 . . . . . . . . . . . . . . . 16 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → 𝑠 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
799, 5fvmptg 6821 . . . . . . . . . . . . . . . . 17 ((𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵) → (𝐻𝑤) = {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)})
8079sseq2d 3938 . . . . . . . . . . . . . . . 16 ((𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵) → (𝑠 ⊆ (𝐻𝑤) ↔ 𝑠 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)}))
8178, 80syl5ibrcom 250 . . . . . . . . . . . . . . 15 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → ((𝑤𝐶 {𝑛𝐵 ∣ (𝑔𝑤) ⊆ (𝑓𝑛)} ∈ 𝐵) → 𝑠 ⊆ (𝐻𝑤)))
8266, 81syl5 34 . . . . . . . . . . . . . 14 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (𝑓𝑠) ⊆ (𝑔𝑤)) → (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → 𝑠 ⊆ (𝐻𝑤)))
8382ex 416 . . . . . . . . . . . . 13 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) → ((𝑓𝑠) ⊆ (𝑔𝑤) → (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → 𝑠 ⊆ (𝐻𝑤))))
8483com23 86 . . . . . . . . . . . 12 (((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) → (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ 𝑤𝐶) → ((𝑓𝑠) ⊆ (𝑔𝑤) → 𝑠 ⊆ (𝐻𝑤))))
8584expdimp 456 . . . . . . . . . . 11 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴)) → (𝑤𝐶 → ((𝑓𝑠) ⊆ (𝑔𝑤) → 𝑠 ⊆ (𝐻𝑤))))
8685reximdvai 3196 . . . . . . . . . 10 ((((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵) ∧ (Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴)) → (∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤) → ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤)))
8786ancoms 462 . . . . . . . . 9 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ ((𝑓 Fn 𝐵 ∧ Smo 𝑓) ∧ 𝑠𝐵)) → (∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤) → ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤)))
8887expr 460 . . . . . . . 8 (((Ord 𝐵 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦) ∧ 𝑔:𝐶𝐴) ∧ (𝑓 Fn 𝐵 ∧ Smo 𝑓)) → (𝑠𝐵 → (∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤) → ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤))))
8920, 21, 22, 63, 64, 88syl32anc 1380 . . . . . . 7 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → (𝑠𝐵 → (∃𝑤𝐶 (𝑓𝑠) ⊆ (𝑔𝑤) → ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤))))
9062, 89mpdd 43 . . . . . 6 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → (𝑠𝐵 → ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤)))
9190ralrimiv 3104 . . . . 5 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝐻𝑤))
92 feq1 6531 . . . . . . . 8 ( = 𝐻 → (:𝐶𝐵𝐻:𝐶𝐵))
93 fveq1 6721 . . . . . . . . . . 11 ( = 𝐻 → (𝑤) = (𝐻𝑤))
9493sseq2d 3938 . . . . . . . . . 10 ( = 𝐻 → (𝑠 ⊆ (𝑤) ↔ 𝑠 ⊆ (𝐻𝑤)))
9594rexbidv 3221 . . . . . . . . 9 ( = 𝐻 → (∃𝑤𝐶 𝑠 ⊆ (𝑤) ↔ ∃𝑤𝐶 𝑠 ⊆ (𝐻𝑤)))
9695ralbidv 3118 . . . . . . . 8 ( = 𝐻 → (∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤) ↔ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝐻𝑤)))
9792, 96anbi12d 634 . . . . . . 7 ( = 𝐻 → ((:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤)) ↔ (𝐻:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝐻𝑤))))
9897spcegv 3517 . . . . . 6 (𝐻 ∈ V → ((𝐻:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝐻𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤))))
99983impib 1118 . . . . 5 ((𝐻 ∈ V ∧ 𝐻:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝐻𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤)))
10015, 53, 91, 99syl3anc 1373 . . . 4 (((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) ∧ (𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤))) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤)))
101100ex 416 . . 3 ((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) → ((𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤))))
102101exlimdv 1941 . 2 ((𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) → (∃𝑔(𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤))))
103102exlimiv 1938 1 (∃𝑓(𝑓:𝐵𝐴 ∧ Smo 𝑓 ∧ ∀𝑥𝐴𝑦𝐵 𝑥 ⊆ (𝑓𝑦)) → (∃𝑔(𝑔:𝐶𝐴 ∧ ∀𝑧𝐴𝑤𝐶 𝑧 ⊆ (𝑔𝑤)) → ∃(:𝐶𝐵 ∧ ∀𝑠𝐵𝑤𝐶 𝑠 ⊆ (𝑤))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3413  wss 3871  c0 4242   cint 4864  cmpt 5140  dom cdm 5556  Ord word 6217  Oncon0 6218   Fn wfn 6380  wf 6381  cfv 6385  Smo wsmo 8087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pr 5327  ax-un 7528
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-ord 6221  df-on 6222  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-smo 8088
This theorem is referenced by:  cfcof  9893
  Copyright terms: Public domain W3C validator