Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
2 | | vex 3176 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
3 | 1, 2 | xpex 6860 |
. . . . . . 7
⊢ (𝑢 × 𝑣) ∈ V |
4 | 3 | rgen2w 2909 |
. . . . . 6
⊢
∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V |
5 | | eqid 2610 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) |
6 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑧 = (𝑢 × 𝑣) → (〈𝑅, 𝑆〉 ∈ 𝑧 ↔ 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣))) |
7 | | sseq2 3590 |
. . . . . . . . 9
⊢ (𝑧 = (𝑢 × 𝑣) → ((𝐻 “ ℎ) ⊆ 𝑧 ↔ (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) |
8 | 7 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑧 = (𝑢 × 𝑣) → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧 ↔ ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) |
9 | 6, 8 | imbi12d 333 |
. . . . . . 7
⊢ (𝑧 = (𝑢 × 𝑣) → ((〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)))) |
10 | 5, 9 | ralrnmpt2 6673 |
. . . . . 6
⊢
(∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)))) |
11 | 4, 10 | ax-mp 5 |
. . . . 5
⊢
(∀𝑧 ∈
ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) |
12 | | opelxp 5070 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣)) |
13 | | ancom 465 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢)) |
14 | 12, 13 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢)) |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢))) |
16 | | r19.40 3069 |
. . . . . . . . . . . . . . . . 17
⊢
(∃ℎ ∈
𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) → (∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) |
17 | | raleq 3115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑓 → (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) |
18 | 17 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢) |
19 | | raleq 3115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑔 → (∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
20 | 19 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) |
21 | 18, 20 | anbi12i 729 |
. . . . . . . . . . . . . . . . 17
⊢
((∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
22 | 16, 21 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢
(∃ℎ ∈
𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) → (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
23 | | reeanv 3086 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑓 ∈
𝐿 ∃𝑔 ∈ 𝐿 (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
24 | | txflf.l |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) |
25 | | filin 21468 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿) → (𝑓 ∩ 𝑔) ∈ 𝐿) |
26 | 25 | 3expb 1258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → (𝑓 ∩ 𝑔) ∈ 𝐿) |
27 | 24, 26 | sylan 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → (𝑓 ∩ 𝑔) ∈ 𝐿) |
28 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∩ 𝑔) ⊆ 𝑓 |
29 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∩ 𝑔) ⊆ 𝑓 → (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑛 ∈
𝑓 (𝐹‘𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢) |
31 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∩ 𝑔) ⊆ 𝑔 |
32 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∩ 𝑔) ⊆ 𝑔 → (∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑛 ∈
𝑔 (𝐺‘𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣) |
34 | 30, 33 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑛 ∈
𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) |
35 | | raleq 3115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑓 ∩ 𝑔) → (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢)) |
36 | | raleq 3115 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑓 ∩ 𝑔) → (∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) |
37 | 35, 36 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑓 ∩ 𝑔) → ((∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣))) |
38 | 37 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∩ 𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) |
39 | 27, 34, 38 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) ∧ (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) |
40 | 39 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → ((∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) |
41 | 40 | rexlimdvva 3020 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑓 ∈ 𝐿 ∃𝑔 ∈ 𝐿 (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) |
42 | 23, 41 | syl5bir 232 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) |
43 | 22, 42 | impbid2 215 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣))) |
44 | | df-ima 5051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 “ ℎ) = ran (𝐻 ↾ ℎ) |
45 | | filelss 21466 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ ℎ ∈ 𝐿) → ℎ ⊆ 𝑍) |
46 | 24, 45 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ℎ ⊆ 𝑍) |
47 | | txflf.h |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) |
48 | 47 | reseq1i 5313 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐻 ↾ ℎ) = ((𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ↾ ℎ) |
49 | | resmpt 5369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ ⊆ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) |
50 | 48, 49 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ⊆ 𝑍 → (𝐻 ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) |
51 | 46, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → (𝐻 ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) |
52 | 51 | rneqd 5274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ran (𝐻 ↾ ℎ) = ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) |
53 | 44, 52 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → (𝐻 “ ℎ) = ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) |
54 | 53 | sseq1d 3595 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ((𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣))) |
55 | | opelxp 5070 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣)) |
56 | 55 | ralbii 2963 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ∈ ℎ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣)) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) |
58 | 57 | fmpt 6289 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣)) |
59 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ V |
60 | 59, 57 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) Fn ℎ |
61 | | df-f 5808 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣) ↔ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) Fn ℎ ∧ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣))) |
62 | 60, 61 | mpbiran 955 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣)) |
63 | 58, 62 | bitri 263 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣)) |
64 | | r19.26 3046 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) |
65 | 56, 63, 64 | 3bitr3i 289 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) |
66 | 54, 65 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ((𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) |
67 | 66 | rexbidva 3031 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) |
68 | | txflf.f |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝐹:𝑍⟶𝑋) |
70 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑍⟶𝑋 → Fun 𝐹) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → Fun 𝐹) |
72 | | filelss 21466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ 𝑍) |
73 | 24, 72 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ 𝑍) |
74 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹:𝑍⟶𝑋 → dom 𝐹 = 𝑍) |
75 | 69, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → dom 𝐹 = 𝑍) |
76 | 73, 75 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ dom 𝐹) |
77 | | funimass4 6157 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐹 ∧ 𝑓 ⊆ dom 𝐹) → ((𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) |
78 | 71, 76, 77 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → ((𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) |
79 | 78 | rexbidva 3031 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) |
80 | | txflf.g |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:𝑍⟶𝑌) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝐺:𝑍⟶𝑌) |
82 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺:𝑍⟶𝑌 → Fun 𝐺) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → Fun 𝐺) |
84 | | filelss 21466 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ 𝑍) |
85 | 24, 84 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ 𝑍) |
86 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:𝑍⟶𝑌 → dom 𝐺 = 𝑍) |
87 | 81, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → dom 𝐺 = 𝑍) |
88 | 85, 87 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ dom 𝐺) |
89 | | funimass4 6157 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐺 ∧ 𝑔 ⊆ dom 𝐺) → ((𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
90 | 83, 88, 89 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → ((𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
91 | 90 | rexbidva 3031 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) |
92 | 79, 91 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣))) |
93 | 43, 67, 92 | 3bitr4d 299 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
94 | 15, 93 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢) → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
95 | | impexp 461 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢) → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
96 | 94, 95 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) |
97 | 96 | ralbidv 2969 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) |
98 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → (𝑆 ∈ 𝑥 ↔ 𝑆 ∈ 𝑣)) |
99 | 98 | ralrab 3335 |
. . . . . . . . . . . 12
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
100 | | r19.21v 2943 |
. . . . . . . . . . . 12
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
101 | 99, 100 | bitr3i 265 |
. . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
102 | 97, 101 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
103 | 102 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
104 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑅 ∈ 𝑥 ↔ 𝑅 ∈ 𝑢)) |
105 | 104 | ralrab 3335 |
. . . . . . . . 9
⊢
(∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
106 | 103, 105 | syl6bbr 277 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
107 | 106 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
108 | | txflf.j |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
109 | | toponmax 20543 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐽) |
111 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑅 ∈ 𝑥 ↔ 𝑅 ∈ 𝑋)) |
112 | 111 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) → ∃𝑥 ∈ 𝐽 𝑅 ∈ 𝑥) |
113 | | rabn0 3912 |
. . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ↔ ∃𝑥 ∈ 𝐽 𝑅 ∈ 𝑥) |
114 | 112, 113 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) → {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅) |
115 | 110, 114 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑋) → {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅) |
116 | | txflf.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
117 | | toponmax 20543 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) |
118 | 116, 117 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐾) |
119 | | eleq2 2677 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → (𝑆 ∈ 𝑥 ↔ 𝑆 ∈ 𝑌)) |
120 | 119 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ 𝐾 ∧ 𝑆 ∈ 𝑌) → ∃𝑥 ∈ 𝐾 𝑆 ∈ 𝑥) |
121 | | rabn0 3912 |
. . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ ↔ ∃𝑥 ∈ 𝐾 𝑆 ∈ 𝑥) |
122 | 120, 121 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ 𝐾 ∧ 𝑆 ∈ 𝑌) → {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) |
123 | 118, 122 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑌) → {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) |
124 | 115, 123 | anim12dan 878 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ∧ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅)) |
125 | | r19.28zv 4018 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
126 | 125 | ralbidv 2969 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
127 | | r19.27zv 4023 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
128 | 126, 127 | sylan9bbr 733 |
. . . . . . . 8
⊢ (({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ∧ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
129 | 124, 128 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
130 | 107, 129 | bitrd 267 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
131 | 104 | ralrab 3335 |
. . . . . . 7
⊢
(∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) |
132 | 98 | ralrab 3335 |
. . . . . . 7
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) |
133 | 131, 132 | anbi12i 729 |
. . . . . 6
⊢
((∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) |
134 | 130, 133 | syl6bb 275 |
. . . . 5
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
135 | 11, 134 | syl5bb 271 |
. . . 4
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
136 | 135 | pm5.32da 671 |
. . 3
⊢ (𝜑 → (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) |
137 | | opelxp 5070 |
. . . 4
⊢
(〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ↔ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) |
138 | 137 | anbi1i 727 |
. . 3
⊢
((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧))) |
139 | | an4 861 |
. . 3
⊢ (((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
140 | 136, 138,
139 | 3bitr4g 302 |
. 2
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) |
141 | | eqid 2610 |
. . . . . . . 8
⊢ ran
(𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) |
142 | 141 | txval 21177 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
143 | 108, 116,
142 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) |
144 | 143 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)) |
145 | 144 | fveq1d 6105 |
. . . 4
⊢ (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)) |
146 | 145 | eleq2d 2673 |
. . 3
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ 〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))) |
147 | | txtopon 21204 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
148 | 108, 116,
147 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) |
149 | 143, 148 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌))) |
150 | 68 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ 𝑋) |
151 | 80 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ 𝑌) |
152 | | opelxpi 5072 |
. . . . . 6
⊢ (((𝐹‘𝑛) ∈ 𝑋 ∧ (𝐺‘𝑛) ∈ 𝑌) → 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑋 × 𝑌)) |
153 | 150, 151,
152 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑋 × 𝑌)) |
154 | 153, 47 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐻:𝑍⟶(𝑋 × 𝑌)) |
155 | | eqid 2610 |
. . . . 5
⊢
(topGen‘ran (𝑢
∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) |
156 | 155 | flftg 21610 |
. . . 4
⊢
(((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) |
157 | 149, 24, 154, 156 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) |
158 | 146, 157 | bitrd 267 |
. 2
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) |
159 | | isflf 21607 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍⟶𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)))) |
160 | 108, 24, 68, 159 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)))) |
161 | | isflf 21607 |
. . . 4
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍⟶𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
162 | 116, 24, 80, 161 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) |
163 | 160, 162 | anbi12d 743 |
. 2
⊢ (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) |
164 | 140, 158,
163 | 3bitr4d 299 |
1
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)))) |