Step | Hyp | Ref
| Expression |
1 | | r19.27v 3112 |
. . . . . . . 8
⊢
((∀𝑢 ∈
𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑢 ∈ 𝐽 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
2 | | r19.28v 3113 |
. . . . . . . . 9
⊢ (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
3 | 2 | ralimi 3089 |
. . . . . . . 8
⊢
(∀𝑢 ∈
𝐽 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢
((∀𝑢 ∈
𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
5 | | simprl 768 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → 𝑤 ∈ (𝐽 ×t 𝐾)) |
6 | | txlm.j |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
7 | | topontop 22060 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐽 ∈ Top) |
9 | | txlm.k |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
10 | | topontop 22060 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ Top) |
12 | | eqid 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) |
13 | 12 | txval 22713 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
14 | 8, 11, 13 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
16 | 5, 15 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → 𝑤 ∈ (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
17 | | simprr 770 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → 〈𝑅, 𝑆〉 ∈ 𝑤) |
18 | | tg2 22113 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤) → ∃𝑡 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤)) |
19 | 16, 17, 18 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → ∃𝑡 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤)) |
20 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑢 ∈ V |
21 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑣 ∈ V |
22 | 20, 21 | xpex 7597 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 × 𝑣) ∈ V |
23 | 22 | rgen2w 3079 |
. . . . . . . . . . . . . 14
⊢
∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V |
24 | | eqid 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) |
25 | | eleq2 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 × 𝑣) → (〈𝑅, 𝑆〉 ∈ 𝑡 ↔ 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣))) |
26 | | sseq1 3951 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = (𝑢 × 𝑣) → (𝑡 ⊆ 𝑤 ↔ (𝑢 × 𝑣) ⊆ 𝑤)) |
27 | 25, 26 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = (𝑢 × 𝑣) → ((〈𝑅, 𝑆〉 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤) ↔ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
28 | 24, 27 | rexrnmpo 7407 |
. . . . . . . . . . . . . 14
⊢
(∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V → (∃𝑡 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
29 | 23, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑡 ∈ ran
(𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑡 ∧ 𝑡 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) |
30 | 19, 29 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) |
31 | 30 | ex 413 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
32 | | r19.29 3186 |
. . . . . . . . . . . . 13
⊢
((∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑢 ∈ 𝐽 (∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
33 | | r19.29 3186 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑣 ∈
𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑣 ∈ 𝐾 (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤))) |
34 | | simprl 768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣)) |
35 | | opelxp 5626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣)) |
36 | 34, 35 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣)) |
37 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ 𝑢 → ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) |
38 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ 𝑣 → ((𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) |
39 | 37, 38 | im2anan9 620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣) → (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
40 | 36, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
41 | | txlm.z |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑍 =
(ℤ≥‘𝑀) |
42 | 41 | rexanuz2 15059 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) |
43 | 41 | uztrn2 12600 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
44 | | opelxpi 5627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → 〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑢 × 𝑣)) |
45 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
46 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → (𝐺‘𝑛) = (𝐺‘𝑘)) |
47 | 45, 46 | opeq12d 4818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 = 〈(𝐹‘𝑘), (𝐺‘𝑘)〉) |
48 | | txlm.h |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) |
49 | | opex 5383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ V |
50 | 47, 48, 49 | fvmpt 6872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈ 𝑍 → (𝐻‘𝑘) = 〈(𝐹‘𝑘), (𝐺‘𝑘)〉) |
51 | 50 | eleq1d 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ 𝑍 → ((𝐻‘𝑘) ∈ (𝑢 × 𝑣) ↔ 〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑢 × 𝑣))) |
52 | 44, 51 | syl5ibr 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ 𝑍 → (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → (𝐻‘𝑘) ∈ (𝑢 × 𝑣))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘 ∈ 𝑍) → (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → (𝐻‘𝑘) ∈ (𝑢 × 𝑣))) |
54 | | simplrr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘 ∈ 𝑍) → (𝑢 × 𝑣) ⊆ 𝑤) |
55 | 54 | sseld 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘 ∈ 𝑍) → ((𝐻‘𝑘) ∈ (𝑢 × 𝑣) → (𝐻‘𝑘) ∈ 𝑤)) |
56 | 53, 55 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑘 ∈ 𝑍) → (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → (𝐻‘𝑘) ∈ 𝑤)) |
57 | 43, 56 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ (𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗))) → (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → (𝐻‘𝑘) ∈ 𝑤)) |
58 | 57 | anassrs 468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → (𝐻‘𝑘) ∈ 𝑤)) |
59 | 58 | ralimdva 3105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
60 | 59 | reximdva 3205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑢 ∧ (𝐺‘𝑘) ∈ 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
61 | 42, 60 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ((∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢 ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
62 | 40, 61 | syld 47 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
63 | 62 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
64 | 63 | impcomd 412 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐾) → ((((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
65 | 64 | rexlimdva 3215 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → (∃𝑣 ∈ 𝐾 (((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
66 | 33, 65 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → ((∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
67 | 66 | rexlimdva 3215 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∃𝑢 ∈ 𝐽 (∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
68 | 32, 67 | syl5 34 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ∧ ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) |
69 | 68 | expcomd 417 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑤) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
70 | 31, 69 | syld 47 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑤 ∈ (𝐽 ×t 𝐾) ∧ 〈𝑅, 𝑆〉 ∈ 𝑤) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
71 | 70 | expdimp 453 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → (〈𝑅, 𝑆〉 ∈ 𝑤 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
72 | 71 | com23 86 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐽 ×t 𝐾)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → (〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
73 | 72 | ralrimdva 3115 |
. . . . . . 7
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 ((𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
74 | 4, 73 | syl5 34 |
. . . . . 6
⊢ (𝜑 → ((∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
75 | 74 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → ((∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) → ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
76 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → 𝐽 ∈ Top) |
77 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → 𝐾 ∈ Top) |
78 | | simprr 770 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → 𝑢 ∈ 𝐽) |
79 | | toponmax 22073 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) |
80 | 9, 79 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
81 | 80 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → 𝑌 ∈ 𝐾) |
82 | | txopn 22751 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑢 ∈ 𝐽 ∧ 𝑌 ∈ 𝐾)) → (𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾)) |
83 | 76, 77, 78, 81, 82 | syl22anc 836 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → (𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾)) |
84 | | eleq2 2829 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑢 × 𝑌) → (〈𝑅, 𝑆〉 ∈ 𝑤 ↔ 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌))) |
85 | | eleq2 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑢 × 𝑌) → ((𝐻‘𝑘) ∈ 𝑤 ↔ (𝐻‘𝑘) ∈ (𝑢 × 𝑌))) |
86 | 85 | rexralbidv 3232 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑢 × 𝑌) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌))) |
87 | 84, 86 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑢 × 𝑌) → ((〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) ↔ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌)))) |
88 | 87 | rspcv 3556 |
. . . . . . . . . . 11
⊢ ((𝑢 × 𝑌) ∈ (𝐽 ×t 𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌)))) |
89 | 83, 88 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌)))) |
90 | | simprl 768 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → 𝑆 ∈ 𝑌) |
91 | | opelxpi 5627 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑌) → 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌)) |
92 | 90, 91 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ 𝑢 ∧ (𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽))) → 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌)) |
93 | 92 | expcom 414 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → (𝑅 ∈ 𝑢 → 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌))) |
94 | 50 | eleq1d 2825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → ((𝐻‘𝑘) ∈ (𝑢 × 𝑌) ↔ 〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑢 × 𝑌))) |
95 | | opelxp1 5631 |
. . . . . . . . . . . . . . . 16
⊢
(〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑢 × 𝑌) → (𝐹‘𝑘) ∈ 𝑢) |
96 | 94, 95 | syl6bi 252 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → ((𝐻‘𝑘) ∈ (𝑢 × 𝑌) → (𝐹‘𝑘) ∈ 𝑢)) |
97 | 43, 96 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐻‘𝑘) ∈ (𝑢 × 𝑌) → (𝐹‘𝑘) ∈ 𝑢)) |
98 | 97 | ralimdva 3105 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) |
99 | 98 | reximia 3175 |
. . . . . . . . . . . 12
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) |
100 | 99 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) |
101 | 93, 100 | imim12d 81 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑌) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑢 × 𝑌)) → (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))) |
102 | 89, 101 | syld 47 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑆 ∈ 𝑌 ∧ 𝑢 ∈ 𝐽)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))) |
103 | 102 | anassrs 468 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑆 ∈ 𝑌) ∧ 𝑢 ∈ 𝐽) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))) |
104 | 103 | ralrimdva 3115 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑌) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))) |
105 | 104 | adantrl 713 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢))) |
106 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → 𝐽 ∈ Top) |
107 | 11 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → 𝐾 ∈ Top) |
108 | | toponmax 22073 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
109 | 6, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
110 | 109 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → 𝑋 ∈ 𝐽) |
111 | | simprr 770 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → 𝑣 ∈ 𝐾) |
112 | | txopn 22751 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑋 ∈ 𝐽 ∧ 𝑣 ∈ 𝐾)) → (𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾)) |
113 | 106, 107,
110, 111, 112 | syl22anc 836 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → (𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾)) |
114 | | eleq2 2829 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑋 × 𝑣) → (〈𝑅, 𝑆〉 ∈ 𝑤 ↔ 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣))) |
115 | | eleq2 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑋 × 𝑣) → ((𝐻‘𝑘) ∈ 𝑤 ↔ (𝐻‘𝑘) ∈ (𝑋 × 𝑣))) |
116 | 115 | rexralbidv 3232 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝑋 × 𝑣) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤 ↔ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣))) |
117 | 114, 116 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑋 × 𝑣) → ((〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣)))) |
118 | 117 | rspcv 3556 |
. . . . . . . . . . 11
⊢ ((𝑋 × 𝑣) ∈ (𝐽 ×t 𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣)))) |
119 | 113, 118 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣)))) |
120 | | opelxpi 5627 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑣) → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣)) |
121 | 120 | ex 413 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ 𝑋 → (𝑆 ∈ 𝑣 → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣))) |
122 | 121 | ad2antrl 725 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → (𝑆 ∈ 𝑣 → 〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣))) |
123 | 50 | eleq1d 2825 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → ((𝐻‘𝑘) ∈ (𝑋 × 𝑣) ↔ 〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑋 × 𝑣))) |
124 | | opelxp2 5632 |
. . . . . . . . . . . . . . . 16
⊢
(〈(𝐹‘𝑘), (𝐺‘𝑘)〉 ∈ (𝑋 × 𝑣) → (𝐺‘𝑘) ∈ 𝑣) |
125 | 123, 124 | syl6bi 252 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → ((𝐻‘𝑘) ∈ (𝑋 × 𝑣) → (𝐺‘𝑘) ∈ 𝑣)) |
126 | 43, 125 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐻‘𝑘) ∈ (𝑋 × 𝑣) → (𝐺‘𝑘) ∈ 𝑣)) |
127 | 126 | ralimdva 3105 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ 𝑍 → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) |
128 | 127 | reximia 3175 |
. . . . . . . . . . . 12
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣) |
129 | 128 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) |
130 | 122, 129 | imim12d 81 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → ((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑣) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ (𝑋 × 𝑣)) → (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
131 | 119, 130 | syld 47 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑣 ∈ 𝐾)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
132 | 131 | anassrs 468 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑅 ∈ 𝑋) ∧ 𝑣 ∈ 𝐾) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
133 | 132 | ralrimdva 3115 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑋) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
134 | 133 | adantrr 714 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) |
135 | 105, 134 | jcad 513 |
. . . . 5
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤) → (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)))) |
136 | 75, 135 | impbid 211 |
. . . 4
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → ((∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)) ↔ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
137 | 136 | pm5.32da 579 |
. . 3
⊢ (𝜑 → (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)))) |
138 | | opelxp 5626 |
. . . 4
⊢
(〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ↔ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) |
139 | 138 | anbi1i 624 |
. . 3
⊢
((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤))) |
140 | 137, 139 | bitr4di 289 |
. 2
⊢ (𝜑 → (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)))) |
141 | | txlm.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
142 | | txlm.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) |
143 | | eqidd 2741 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
144 | 6, 41, 141, 142, 143 | lmbrf 22409 |
. . . 4
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑅 ↔ (𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)))) |
145 | | txlm.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝑍⟶𝑌) |
146 | | eqidd 2741 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
147 | 9, 41, 141, 145, 146 | lmbrf 22409 |
. . . 4
⊢ (𝜑 → (𝐺(⇝𝑡‘𝐾)𝑆 ↔ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)))) |
148 | 144, 147 | anbi12d 631 |
. . 3
⊢ (𝜑 → ((𝐹(⇝𝑡‘𝐽)𝑅 ∧ 𝐺(⇝𝑡‘𝐾)𝑆) ↔ ((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))))) |
149 | | an4 653 |
. . 3
⊢ (((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣)))) |
150 | 148, 149 | bitrdi 287 |
. 2
⊢ (𝜑 → ((𝐹(⇝𝑡‘𝐽)𝑅 ∧ 𝐺(⇝𝑡‘𝐾)𝑆) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐺‘𝑘) ∈ 𝑣))))) |
151 | | txtopon 22740 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
152 | 6, 9, 151 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
153 | 142 | ffvelrnda 6958 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ 𝑋) |
154 | 145 | ffvelrnda 6958 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ 𝑌) |
155 | 153, 154 | opelxpd 5628 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑋 × 𝑌)) |
156 | 155, 48 | fmptd 6985 |
. . 3
⊢ (𝜑 → 𝐻:𝑍⟶(𝑋 × 𝑌)) |
157 | | eqidd 2741 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐻‘𝑘) = (𝐻‘𝑘)) |
158 | 152, 41, 141, 156, 157 | lmbrf 22409 |
. 2
⊢ (𝜑 → (𝐻(⇝𝑡‘(𝐽 ×t 𝐾))〈𝑅, 𝑆〉 ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑤 ∈ (𝐽 ×t 𝐾)(〈𝑅, 𝑆〉 ∈ 𝑤 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐻‘𝑘) ∈ 𝑤)))) |
159 | 140, 150,
158 | 3bitr4d 311 |
1
⊢ (𝜑 → ((𝐹(⇝𝑡‘𝐽)𝑅 ∧ 𝐺(⇝𝑡‘𝐾)𝑆) ↔ 𝐻(⇝𝑡‘(𝐽 ×t 𝐾))〈𝑅, 𝑆〉)) |