Step | Hyp | Ref
| Expression |
1 | | cvmlift2.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
2 | | cvmlift2.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
3 | | iitop 22491 |
. . . . . . 7
⊢ II ∈
Top |
4 | | iiuni 22492 |
. . . . . . 7
⊢ (0[,]1) =
∪ II |
5 | 3, 3, 4, 4 | txunii 21206 |
. . . . . 6
⊢ ((0[,]1)
× (0[,]1)) = ∪ (II ×t
II) |
6 | | eqid 2610 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
7 | 5, 6 | cnf 20860 |
. . . . 5
⊢ (𝐺 ∈ ((II ×t
II) Cn 𝐽) → 𝐺:((0[,]1) ×
(0[,]1))⟶∪ 𝐽) |
8 | 2, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:((0[,]1) × (0[,]1))⟶∪ 𝐽) |
9 | | cvmlift2lem10.1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (0[,]1)) |
10 | | cvmlift2lem10.2 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (0[,]1)) |
11 | | opelxpi 5072 |
. . . . 5
⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) →
〈𝑋, 𝑌〉 ∈ ((0[,]1) ×
(0[,]1))) |
12 | 9, 10, 11 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ ((0[,]1) ×
(0[,]1))) |
13 | 8, 12 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐺‘〈𝑋, 𝑌〉) ∈ ∪
𝐽) |
14 | | cvmlift2lem10.s |
. . . 4
⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 =
(◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾t 𝑐)Homeo(𝐽 ↾t 𝑘))))}) |
15 | 14, 6 | cvmcov 30499 |
. . 3
⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺‘〈𝑋, 𝑌〉) ∈ ∪
𝐽) → ∃𝑚 ∈ 𝐽 ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ (𝑆‘𝑚) ≠ ∅)) |
16 | 1, 13, 15 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑚 ∈ 𝐽 ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ (𝑆‘𝑚) ≠ ∅)) |
17 | | n0 3890 |
. . . . 5
⊢ ((𝑆‘𝑚) ≠ ∅ ↔ ∃𝑡 𝑡 ∈ (𝑆‘𝑚)) |
18 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → 〈𝑋, 𝑌〉 ∈ ((0[,]1) ×
(0[,]1))) |
19 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚) |
20 | 8 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → 𝐺:((0[,]1) × (0[,]1))⟶∪ 𝐽) |
21 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝐺:((0[,]1) ×
(0[,]1))⟶∪ 𝐽 → 𝐺 Fn ((0[,]1) ×
(0[,]1))) |
22 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn ((0[,]1) × (0[,]1))
→ (〈𝑋, 𝑌〉 ∈ (◡𝐺 “ 𝑚) ↔ (〈𝑋, 𝑌〉 ∈ ((0[,]1) × (0[,]1))
∧ (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚))) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → (〈𝑋, 𝑌〉 ∈ (◡𝐺 “ 𝑚) ↔ (〈𝑋, 𝑌〉 ∈ ((0[,]1) × (0[,]1))
∧ (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚))) |
24 | 18, 19, 23 | mpbir2and 959 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → 〈𝑋, 𝑌〉 ∈ (◡𝐺 “ 𝑚)) |
25 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
26 | 14 | cvmsrcl 30500 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (𝑆‘𝑚) → 𝑚 ∈ 𝐽) |
27 | 26 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → 𝑚 ∈ 𝐽) |
28 | | cnima 20879 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ ((II ×t
II) Cn 𝐽) ∧ 𝑚 ∈ 𝐽) → (◡𝐺 “ 𝑚) ∈ (II ×t
II)) |
29 | 25, 27, 28 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → (◡𝐺 “ 𝑚) ∈ (II ×t
II)) |
30 | | eltx 21181 |
. . . . . . . . . . . 12
⊢ ((II
∈ Top ∧ II ∈ Top) → ((◡𝐺 “ 𝑚) ∈ (II ×t II) ↔
∀𝑧 ∈ (◡𝐺 “ 𝑚)∃𝑎 ∈ II ∃𝑏 ∈ II (𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)))) |
31 | 3, 3, 30 | mp2an 704 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ 𝑚) ∈ (II ×t II) ↔
∀𝑧 ∈ (◡𝐺 “ 𝑚)∃𝑎 ∈ II ∃𝑏 ∈ II (𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) |
32 | 29, 31 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → ∀𝑧 ∈ (◡𝐺 “ 𝑚)∃𝑎 ∈ II ∃𝑏 ∈ II (𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) |
33 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 〈𝑋, 𝑌〉 → (𝑧 ∈ (𝑎 × 𝑏) ↔ 〈𝑋, 𝑌〉 ∈ (𝑎 × 𝑏))) |
34 | | opelxp 5070 |
. . . . . . . . . . . . . 14
⊢
(〈𝑋, 𝑌〉 ∈ (𝑎 × 𝑏) ↔ (𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏)) |
35 | 33, 34 | syl6bb 275 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑋, 𝑌〉 → (𝑧 ∈ (𝑎 × 𝑏) ↔ (𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏))) |
36 | 35 | anbi1d 737 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑋, 𝑌〉 → ((𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) ↔ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)))) |
37 | 36 | 2rexbidv 3039 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑋, 𝑌〉 → (∃𝑎 ∈ II ∃𝑏 ∈ II (𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) ↔ ∃𝑎 ∈ II ∃𝑏 ∈ II ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)))) |
38 | 37 | rspcv 3278 |
. . . . . . . . . 10
⊢
(〈𝑋, 𝑌〉 ∈ (◡𝐺 “ 𝑚) → (∀𝑧 ∈ (◡𝐺 “ 𝑚)∃𝑎 ∈ II ∃𝑏 ∈ II (𝑧 ∈ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) → ∃𝑎 ∈ II ∃𝑏 ∈ II ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)))) |
39 | 24, 32, 38 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → ∃𝑎 ∈ II ∃𝑏 ∈ II ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) |
40 | | iillyscon 30489 |
. . . . . . . . . . . . . 14
⊢ II ∈
Locally SCon |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → II ∈ Locally
SCon) |
42 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → 𝑎 ∈ II) |
43 | | simprll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → 𝑋 ∈ 𝑎) |
44 | | llyi 21087 |
. . . . . . . . . . . . 13
⊢ ((II
∈ Locally SCon ∧ 𝑎
∈ II ∧ 𝑋 ∈
𝑎) → ∃𝑢 ∈ II (𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon)) |
45 | 41, 42, 43, 44 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → ∃𝑢 ∈ II (𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon)) |
46 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → 𝑏 ∈ II) |
47 | | simprlr 799 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → 𝑌 ∈ 𝑏) |
48 | | llyi 21087 |
. . . . . . . . . . . . 13
⊢ ((II
∈ Locally SCon ∧ 𝑏
∈ II ∧ 𝑌 ∈
𝑏) → ∃𝑣 ∈ II (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) |
49 | 41, 46, 47, 48 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → ∃𝑣 ∈ II (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) |
50 | | reeanv 3086 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈ II
∃𝑣 ∈ II ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) ↔
(∃𝑢 ∈ II (𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧
∃𝑣 ∈ II (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈
SCon))) |
51 | | simpl2 1058 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → 𝑋 ∈ 𝑢) |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → 𝑋 ∈ 𝑢)) |
53 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → 𝑌 ∈ 𝑣) |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → 𝑌 ∈ 𝑣)) |
55 | | simprl1 1099 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) ∧ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon))) → 𝑢 ⊆ 𝑎) |
56 | | simprr1 1102 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) ∧ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon))) → 𝑣 ⊆ 𝑏) |
57 | | xpss12 5148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ⊆ 𝑎 ∧ 𝑣 ⊆ 𝑏) → (𝑢 × 𝑣) ⊆ (𝑎 × 𝑏)) |
58 | 55, 56, 57 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) ∧ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon))) → (𝑢 × 𝑣) ⊆ (𝑎 × 𝑏)) |
59 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) ∧ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon))) → (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) |
60 | 58, 59 | sstrd 3578 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) ∧ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon))) → (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) |
61 | 60 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚))) |
62 | 52, 54, 61 | 3jcad 1236 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)))) |
63 | | simp3 1056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) → (II
↾t 𝑢)
∈ SCon) |
64 | | simp3 1056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon) → (II
↾t 𝑣)
∈ SCon) |
65 | 63, 64 | anim12i 588 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → ((II
↾t 𝑢)
∈ SCon ∧ (II ↾t 𝑣) ∈ SCon)) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → ((II
↾t 𝑢)
∈ SCon ∧ (II ↾t 𝑣) ∈ SCon))) |
67 | 62, 66 | jcad 554 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) → ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
68 | 67 | reximdv 2999 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (∃𝑣 ∈ II ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) →
∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
69 | 68 | reximdv 2999 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → (∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧ (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) →
∃𝑢 ∈ II
∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
70 | 50, 69 | syl5bir 232 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → ((∃𝑢 ∈ II (𝑢 ⊆ 𝑎 ∧ 𝑋 ∈ 𝑢 ∧ (II ↾t 𝑢) ∈ SCon) ∧
∃𝑣 ∈ II (𝑣 ⊆ 𝑏 ∧ 𝑌 ∈ 𝑣 ∧ (II ↾t 𝑣) ∈ SCon)) →
∃𝑢 ∈ II
∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
71 | 45, 49, 70 | mp2and 711 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) ∧ ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚))) → ∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) |
72 | 71 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑎 ∈ II ∧ 𝑏 ∈ II)) → (((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) → ∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
73 | 72 | rexlimdvva 3020 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → (∃𝑎 ∈ II ∃𝑏 ∈ II ((𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑏) ∧ (𝑎 × 𝑏) ⊆ (◡𝐺 “ 𝑚)) → ∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)))) |
74 | 39, 73 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → ∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) |
75 | | simp3l1 1159 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → 𝑋
∈ 𝑢) |
76 | | simp3l2 1160 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → 𝑌
∈ 𝑣) |
77 | | cvmlift2.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = ∪
𝐶 |
78 | | simpl1l 1105 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝜑) |
79 | 78, 1 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝐹 ∈ (𝐶 CovMap 𝐽)) |
80 | 78, 2 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝐺 ∈ ((II ×t II) Cn
𝐽)) |
81 | | cvmlift2.p |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ 𝐵) |
82 | 78, 81 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑃 ∈ 𝐵) |
83 | | cvmlift2.i |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘𝑃) = (0𝐺0)) |
84 | 78, 83 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝐹‘𝑃) = (0𝐺0)) |
85 | | cvmlift2.h |
. . . . . . . . . . . . . . 15
⊢ 𝐻 = (℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑧𝐺0)) ∧ (𝑓‘0) = 𝑃)) |
86 | | cvmlift2.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ ((℩𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = (𝑧 ∈ (0[,]1) ↦ (𝑥𝐺𝑧)) ∧ (𝑓‘0) = (𝐻‘𝑥)))‘𝑦)) |
87 | | df-ov 6552 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋𝐺𝑌) = (𝐺‘〈𝑋, 𝑌〉) |
88 | | simpl1r 1106 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) |
89 | 88 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚) |
90 | 87, 89 | syl5eqel 2692 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝑋𝐺𝑌) ∈ 𝑚) |
91 | 88 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑡 ∈ (𝑆‘𝑚)) |
92 | | simpl2l 1107 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑢 ∈ II) |
93 | | simpl2r 1108 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑣 ∈ II) |
94 | | simp3rl 1127 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → (II ↾t 𝑢) ∈ SCon) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (II
↾t 𝑢)
∈ SCon) |
96 | | sconpcon 30463 |
. . . . . . . . . . . . . . . 16
⊢ ((II
↾t 𝑢)
∈ SCon → (II ↾t 𝑢) ∈ PCon) |
97 | | pconcon 30467 |
. . . . . . . . . . . . . . . 16
⊢ ((II
↾t 𝑢)
∈ PCon → (II ↾t 𝑢) ∈ Con) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (II
↾t 𝑢)
∈ Con) |
99 | | simp3rr 1128 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → (II ↾t 𝑣) ∈ SCon) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (II
↾t 𝑣)
∈ SCon) |
101 | | sconpcon 30463 |
. . . . . . . . . . . . . . . 16
⊢ ((II
↾t 𝑣)
∈ SCon → (II ↾t 𝑣) ∈ PCon) |
102 | | pconcon 30467 |
. . . . . . . . . . . . . . . 16
⊢ ((II
↾t 𝑣)
∈ PCon → (II ↾t 𝑣) ∈ Con) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (II
↾t 𝑣)
∈ Con) |
104 | 75 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑋 ∈ 𝑢) |
105 | 76 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑌 ∈ 𝑣) |
106 | | simp3l3 1161 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → (𝑢
× 𝑣) ⊆ (◡𝐺 “ 𝑚)) |
107 | 106 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) |
108 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → 𝑤 ∈ 𝑣) |
109 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶)) |
110 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(℩𝑏
∈ 𝑡 (𝑋𝐾𝑌) ∈ 𝑏) = (℩𝑏 ∈ 𝑡 (𝑋𝐾𝑌) ∈ 𝑏) |
111 | 77, 79, 80, 82, 84, 85, 86, 14, 90, 91, 92, 93, 98, 103, 104, 105, 107, 108, 109, 110 | cvmlift2lem9 30547 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) ∧ (𝑤
∈ 𝑣 ∧ (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶))) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)) |
112 | 111 | rexlimdvaa 3014 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))) |
113 | 75, 76, 112 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II) ∧ ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon))) → (𝑋
∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
114 | 113 | 3expia 1259 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ (𝑢 ∈ II ∧ 𝑣 ∈ II)) → (((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)) → (𝑋
∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
115 | 114 | anassrs 678 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ 𝑢 ∈ II) ∧ 𝑣 ∈ II) → (((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)) → (𝑋
∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
116 | 115 | reximdva 3000 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) ∧ 𝑢 ∈ II) → (∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)) → ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
117 | 116 | reximdva 3000 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → (∃𝑢 ∈ II ∃𝑣 ∈ II ((𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐺 “ 𝑚)) ∧ ((II ↾t 𝑢) ∈ SCon ∧ (II
↾t 𝑣)
∈ SCon)) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
118 | 74, 117 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ 𝑡 ∈ (𝑆‘𝑚))) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |
119 | 118 | expr 641 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚) → (𝑡 ∈ (𝑆‘𝑚) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
120 | 119 | exlimdv 1848 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚) → (∃𝑡 𝑡 ∈ (𝑆‘𝑚) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
121 | 17, 120 | syl5bi 231 |
. . . 4
⊢ ((𝜑 ∧ (𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚) → ((𝑆‘𝑚) ≠ ∅ → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
122 | 121 | expimpd 627 |
. . 3
⊢ (𝜑 → (((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ (𝑆‘𝑚) ≠ ∅) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
123 | 122 | rexlimdvw 3016 |
. 2
⊢ (𝜑 → (∃𝑚 ∈ 𝐽 ((𝐺‘〈𝑋, 𝑌〉) ∈ 𝑚 ∧ (𝑆‘𝑚) ≠ ∅) → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶))))) |
124 | 16, 123 | mpd 15 |
1
⊢ (𝜑 → ∃𝑢 ∈ II ∃𝑣 ∈ II (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ (∃𝑤 ∈ 𝑣 (𝐾 ↾ (𝑢 × {𝑤})) ∈ (((II ×t II)
↾t (𝑢
× {𝑤})) Cn 𝐶) → (𝐾 ↾ (𝑢 × 𝑣)) ∈ (((II ×t II)
↾t (𝑢
× 𝑣)) Cn 𝐶)))) |