| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vex 3483 | . . . . . . . 8
⊢ 𝑢 ∈ V | 
| 2 |  | vex 3483 | . . . . . . . 8
⊢ 𝑣 ∈ V | 
| 3 | 1, 2 | xpex 7774 | . . . . . . 7
⊢ (𝑢 × 𝑣) ∈ V | 
| 4 | 3 | rgen2w 3065 | . . . . . 6
⊢
∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V | 
| 5 |  | eqid 2736 | . . . . . . 7
⊢ (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) | 
| 6 |  | eleq2 2829 | . . . . . . . 8
⊢ (𝑧 = (𝑢 × 𝑣) → (〈𝑅, 𝑆〉 ∈ 𝑧 ↔ 〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣))) | 
| 7 |  | sseq2 4009 | . . . . . . . . 9
⊢ (𝑧 = (𝑢 × 𝑣) → ((𝐻 “ ℎ) ⊆ 𝑧 ↔ (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) | 
| 8 | 7 | rexbidv 3178 | . . . . . . . 8
⊢ (𝑧 = (𝑢 × 𝑣) → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧 ↔ ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) | 
| 9 | 6, 8 | imbi12d 344 | . . . . . . 7
⊢ (𝑧 = (𝑢 × 𝑣) → ((〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)))) | 
| 10 | 5, 9 | ralrnmpo 7573 | . . . . . 6
⊢
(∀𝑢 ∈
𝐽 ∀𝑣 ∈ 𝐾 (𝑢 × 𝑣) ∈ V → (∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)))) | 
| 11 | 4, 10 | ax-mp 5 | . . . . 5
⊢
(∀𝑧 ∈
ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ ∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣))) | 
| 12 |  | opelxp 5720 | . . . . . . . . . . . . . . . 16
⊢
(〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑅 ∈ 𝑢 ∧ 𝑆 ∈ 𝑣)) | 
| 13 | 12 | biancomi 462 | . . . . . . . . . . . . . . 15
⊢
(〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢)) | 
| 14 | 13 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) ↔ (𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢))) | 
| 15 |  | r19.40 3118 | . . . . . . . . . . . . . . . . 17
⊢
(∃ℎ ∈
𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) → (∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) | 
| 16 |  | raleq 3322 | . . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑓 → (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) | 
| 17 | 16 | cbvrexvw 3237 | . . . . . . . . . . . . . . . . . 18
⊢
(∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢) | 
| 18 |  | raleq 3322 | . . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑔 → (∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 19 | 18 | cbvrexvw 3237 | . . . . . . . . . . . . . . . . . 18
⊢
(∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) | 
| 20 | 17, 19 | anbi12i 628 | . . . . . . . . . . . . . . . . 17
⊢
((∃ℎ ∈
𝐿 ∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∃ℎ ∈ 𝐿 ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 21 | 15, 20 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢
(∃ℎ ∈
𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) → (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 22 |  | reeanv 3228 | . . . . . . . . . . . . . . . . 17
⊢
(∃𝑓 ∈
𝐿 ∃𝑔 ∈ 𝐿 (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 23 |  | txflf.l | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) | 
| 24 |  | filin 23863 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿) → (𝑓 ∩ 𝑔) ∈ 𝐿) | 
| 25 | 24 | 3expb 1120 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → (𝑓 ∩ 𝑔) ∈ 𝐿) | 
| 26 | 23, 25 | sylan 580 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → (𝑓 ∩ 𝑔) ∈ 𝐿) | 
| 27 |  | inss1 4236 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∩ 𝑔) ⊆ 𝑓 | 
| 28 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∩ 𝑔) ⊆ 𝑓 → (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢)) | 
| 29 | 27, 28 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑛 ∈
𝑓 (𝐹‘𝑛) ∈ 𝑢 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢) | 
| 30 |  | inss2 4237 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∩ 𝑔) ⊆ 𝑔 | 
| 31 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∩ 𝑔) ⊆ 𝑔 → (∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) | 
| 32 | 30, 31 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑛 ∈
𝑔 (𝐺‘𝑛) ∈ 𝑣 → ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣) | 
| 33 | 29, 32 | anim12i 613 | . . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑛 ∈
𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) | 
| 34 |  | raleq 3322 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑓 ∩ 𝑔) → (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ↔ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢)) | 
| 35 |  | raleq 3322 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = (𝑓 ∩ 𝑔) → (∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣 ↔ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) | 
| 36 | 34, 35 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = (𝑓 ∩ 𝑔) → ((∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣))) | 
| 37 | 36 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∩ 𝑔) ∈ 𝐿 ∧ (∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ (𝑓 ∩ 𝑔)(𝐺‘𝑛) ∈ 𝑣)) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) | 
| 38 | 26, 33, 37 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) ∧ (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) | 
| 39 | 38 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑓 ∈ 𝐿 ∧ 𝑔 ∈ 𝐿)) → ((∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) | 
| 40 | 39 | rexlimdvva 3212 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑓 ∈ 𝐿 ∃𝑔 ∈ 𝐿 (∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) | 
| 41 | 22, 40 | biimtrrid 243 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣) → ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) | 
| 42 | 21, 41 | impbid2 226 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣))) | 
| 43 |  | df-ima 5697 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 “ ℎ) = ran (𝐻 ↾ ℎ) | 
| 44 |  | filelss 23861 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ ℎ ∈ 𝐿) → ℎ ⊆ 𝑍) | 
| 45 | 23, 44 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ℎ ⊆ 𝑍) | 
| 46 |  | txflf.h | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) | 
| 47 | 46 | reseq1i 5992 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐻 ↾ ℎ) = ((𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ↾ ℎ) | 
| 48 |  | resmpt 6054 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ ⊆ 𝑍 → ((𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) | 
| 49 | 47, 48 | eqtrid 2788 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ⊆ 𝑍 → (𝐻 ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) | 
| 50 | 45, 49 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → (𝐻 ↾ ℎ) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) | 
| 51 | 50 | rneqd 5948 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ran (𝐻 ↾ ℎ) = ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) | 
| 52 | 43, 51 | eqtrid 2788 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → (𝐻 “ ℎ) = ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉)) | 
| 53 | 52 | sseq1d 4014 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ((𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣))) | 
| 54 |  | opelxp 5720 | . . . . . . . . . . . . . . . . . . 19
⊢
(〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣)) | 
| 55 | 54 | ralbii 3092 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ∀𝑛 ∈ ℎ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣)) | 
| 56 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) = (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) | 
| 57 | 56 | fmpt 7129 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣)) | 
| 58 |  | opex 5468 | . . . . . . . . . . . . . . . . . . . . 21
⊢
〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ V | 
| 59 | 58, 56 | fnmpti 6710 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) Fn ℎ | 
| 60 |  | df-f 6564 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣) ↔ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) Fn ℎ ∧ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣))) | 
| 61 | 59, 60 | mpbiran 709 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉):ℎ⟶(𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣)) | 
| 62 | 57, 61 | bitri 275 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑢 × 𝑣) ↔ ran (𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣)) | 
| 63 |  | r19.26 3110 | . . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ℎ ((𝐹‘𝑛) ∈ 𝑢 ∧ (𝐺‘𝑛) ∈ 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) | 
| 64 | 55, 62, 63 | 3bitr3i 301 | . . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑛 ∈ ℎ ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣)) | 
| 65 | 53, 64 | bitrdi 287 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ℎ ∈ 𝐿) → ((𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) | 
| 66 | 65 | rexbidva 3176 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ ∃ℎ ∈ 𝐿 (∀𝑛 ∈ ℎ (𝐹‘𝑛) ∈ 𝑢 ∧ ∀𝑛 ∈ ℎ (𝐺‘𝑛) ∈ 𝑣))) | 
| 67 |  | txflf.f | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝐹:𝑍⟶𝑋) | 
| 69 | 68 | ffund 6739 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → Fun 𝐹) | 
| 70 |  | filelss 23861 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ 𝑍) | 
| 71 | 23, 70 | sylan 580 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ 𝑍) | 
| 72 | 68 | fdmd 6745 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → dom 𝐹 = 𝑍) | 
| 73 | 71, 72 | sseqtrrd 4020 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → 𝑓 ⊆ dom 𝐹) | 
| 74 |  | funimass4 6972 | . . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐹 ∧ 𝑓 ⊆ dom 𝐹) → ((𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) | 
| 75 | 69, 73, 74 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐿) → ((𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) | 
| 76 | 75 | rexbidva 3176 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢)) | 
| 77 |  | txflf.g | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:𝑍⟶𝑌) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝐺:𝑍⟶𝑌) | 
| 79 | 78 | ffund 6739 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → Fun 𝐺) | 
| 80 |  | filelss 23861 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐿 ∈ (Fil‘𝑍) ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ 𝑍) | 
| 81 | 23, 80 | sylan 580 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ 𝑍) | 
| 82 | 78 | fdmd 6745 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → dom 𝐺 = 𝑍) | 
| 83 | 81, 82 | sseqtrrd 4020 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → 𝑔 ⊆ dom 𝐺) | 
| 84 |  | funimass4 6972 | . . . . . . . . . . . . . . . . . 18
⊢ ((Fun
𝐺 ∧ 𝑔 ⊆ dom 𝐺) → ((𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 85 | 79, 83, 84 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ 𝐿) → ((𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 86 | 85 | rexbidva 3176 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣)) | 
| 87 | 76, 86 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∃𝑓 ∈ 𝐿 ∀𝑛 ∈ 𝑓 (𝐹‘𝑛) ∈ 𝑢 ∧ ∃𝑔 ∈ 𝐿 ∀𝑛 ∈ 𝑔 (𝐺‘𝑛) ∈ 𝑣))) | 
| 88 | 42, 66, 87 | 3bitr4d 311 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣) ↔ (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 89 | 14, 88 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢) → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 90 |  | impexp 450 | . . . . . . . . . . . . 13
⊢ (((𝑆 ∈ 𝑣 ∧ 𝑅 ∈ 𝑢) → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 91 | 89, 90 | bitrdi 287 | . . . . . . . . . . . 12
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) | 
| 92 | 91 | ralbidv 3177 | . . . . . . . . . . 11
⊢ (𝜑 → (∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) | 
| 93 |  | eleq2 2829 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → (𝑆 ∈ 𝑥 ↔ 𝑆 ∈ 𝑣)) | 
| 94 | 93 | ralrab 3698 | . . . . . . . . . . . 12
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 95 |  | r19.21v 3179 | . . . . . . . . . . . 12
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 96 | 94, 95 | bitr3i 277 | . . . . . . . . . . 11
⊢
(∀𝑣 ∈
𝐾 (𝑆 ∈ 𝑣 → (𝑅 ∈ 𝑢 → (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 97 | 92, 96 | bitrdi 287 | . . . . . . . . . 10
⊢ (𝜑 → (∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 98 | 97 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 99 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑅 ∈ 𝑥 ↔ 𝑅 ∈ 𝑢)) | 
| 100 | 99 | ralrab 3698 | . . . . . . . . 9
⊢
(∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 101 | 98, 100 | bitr4di 289 | . . . . . . . 8
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 102 | 101 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 103 |  | txflf.j | . . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 104 |  | toponmax 22933 | . . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | 
| 105 | 103, 104 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐽) | 
| 106 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑅 ∈ 𝑥 ↔ 𝑅 ∈ 𝑋)) | 
| 107 | 106 | rspcev 3621 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) → ∃𝑥 ∈ 𝐽 𝑅 ∈ 𝑥) | 
| 108 |  | rabn0 4388 | . . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ↔ ∃𝑥 ∈ 𝐽 𝑅 ∈ 𝑥) | 
| 109 | 107, 108 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐽 ∧ 𝑅 ∈ 𝑋) → {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅) | 
| 110 | 105, 109 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑅 ∈ 𝑋) → {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅) | 
| 111 |  | txflf.k | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 112 |  | toponmax 22933 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾) | 
| 113 | 111, 112 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐾) | 
| 114 |  | eleq2 2829 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → (𝑆 ∈ 𝑥 ↔ 𝑆 ∈ 𝑌)) | 
| 115 | 114 | rspcev 3621 | . . . . . . . . . . 11
⊢ ((𝑌 ∈ 𝐾 ∧ 𝑆 ∈ 𝑌) → ∃𝑥 ∈ 𝐾 𝑆 ∈ 𝑥) | 
| 116 |  | rabn0 4388 | . . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ ↔ ∃𝑥 ∈ 𝐾 𝑆 ∈ 𝑥) | 
| 117 | 115, 116 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝑌 ∈ 𝐾 ∧ 𝑆 ∈ 𝑌) → {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) | 
| 118 | 113, 117 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑌) → {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) | 
| 119 | 110, 118 | anim12dan 619 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ∧ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅)) | 
| 120 |  | r19.28zv 4500 | . . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ → (∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 121 | 120 | ralbidv 3177 | . . . . . . . . 9
⊢ ({𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 122 |  | r19.27zv 4505 | . . . . . . . . 9
⊢ ({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 123 | 121, 122 | sylan9bbr 510 | . . . . . . . 8
⊢ (({𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥} ≠ ∅ ∧ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} ≠ ∅) → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 124 | 119, 123 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥} (∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 125 | 102, 124 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 126 | 99 | ralrab 3698 | . . . . . . 7
⊢
(∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ↔ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) | 
| 127 | 93 | ralrab 3698 | . . . . . . 7
⊢
(∀𝑣 ∈
{𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣 ↔ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)) | 
| 128 | 126, 127 | anbi12i 628 | . . . . . 6
⊢
((∀𝑢 ∈
{𝑥 ∈ 𝐽 ∣ 𝑅 ∈ 𝑥}∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢 ∧ ∀𝑣 ∈ {𝑥 ∈ 𝐾 ∣ 𝑆 ∈ 𝑥}∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) | 
| 129 | 125, 128 | bitrdi 287 | . . . . 5
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑢 ∈ 𝐽 ∀𝑣 ∈ 𝐾 (〈𝑅, 𝑆〉 ∈ (𝑢 × 𝑣) → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ (𝑢 × 𝑣)) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 130 | 11, 129 | bitrid 283 | . . . 4
⊢ ((𝜑 ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) → (∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧) ↔ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 131 | 130 | pm5.32da 579 | . . 3
⊢ (𝜑 → (((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) | 
| 132 |  | opelxp 5720 | . . . 4
⊢
(〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ↔ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌)) | 
| 133 | 132 | anbi1i 624 | . . 3
⊢
((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧))) | 
| 134 |  | an4 656 | . . 3
⊢ (((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))) ↔ ((𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝑌) ∧ (∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢) ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 135 | 131, 133,
134 | 3bitr4g 314 | . 2
⊢ (𝜑 → ((〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)) ↔ ((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) | 
| 136 |  | eqid 2736 | . . . . . . . 8
⊢ ran
(𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) = ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)) | 
| 137 | 136 | txval 23573 | . . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) | 
| 138 | 103, 111,
137 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣)))) | 
| 139 | 138 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((𝐽 ×t 𝐾) fLimf 𝐿) = ((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)) | 
| 140 | 139 | fveq1d 6907 | . . . 4
⊢ (𝜑 → (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) = (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻)) | 
| 141 | 140 | eleq2d 2826 | . . 3
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ 〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻))) | 
| 142 |  | txtopon 23600 | . . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 143 | 103, 111,
142 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝐽 ×t 𝐾) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 144 | 138, 143 | eqeltrrd 2841 | . . . 4
⊢ (𝜑 → (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌))) | 
| 145 | 67 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ 𝑋) | 
| 146 | 77 | ffvelcdmda 7103 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ 𝑌) | 
| 147 | 145, 146 | opelxpd 5723 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 〈(𝐹‘𝑛), (𝐺‘𝑛)〉 ∈ (𝑋 × 𝑌)) | 
| 148 | 147, 46 | fmptd 7133 | . . . 4
⊢ (𝜑 → 𝐻:𝑍⟶(𝑋 × 𝑌)) | 
| 149 |  | eqid 2736 | . . . . 5
⊢
(topGen‘ran (𝑢
∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) = (topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) | 
| 150 | 149 | flftg 24005 | . . . 4
⊢
(((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐻:𝑍⟶(𝑋 × 𝑌)) → (〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) | 
| 151 | 144, 23, 148, 150 | syl3anc 1372 | . . 3
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((topGen‘ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) | 
| 152 | 141, 151 | bitrd 279 | . 2
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (〈𝑅, 𝑆〉 ∈ (𝑋 × 𝑌) ∧ ∀𝑧 ∈ ran (𝑢 ∈ 𝐽, 𝑣 ∈ 𝐾 ↦ (𝑢 × 𝑣))(〈𝑅, 𝑆〉 ∈ 𝑧 → ∃ℎ ∈ 𝐿 (𝐻 “ ℎ) ⊆ 𝑧)))) | 
| 153 |  | isflf 24002 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐹:𝑍⟶𝑋) → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)))) | 
| 154 | 103, 23, 67, 153 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)))) | 
| 155 |  | isflf 24002 | . . . 4
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐿 ∈ (Fil‘𝑍) ∧ 𝐺:𝑍⟶𝑌) → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 156 | 111, 23, 77, 155 | syl3anc 1372 | . . 3
⊢ (𝜑 → (𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺) ↔ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣)))) | 
| 157 | 154, 156 | anbi12d 632 | . 2
⊢ (𝜑 → ((𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)) ↔ ((𝑅 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑅 ∈ 𝑢 → ∃𝑓 ∈ 𝐿 (𝐹 “ 𝑓) ⊆ 𝑢)) ∧ (𝑆 ∈ 𝑌 ∧ ∀𝑣 ∈ 𝐾 (𝑆 ∈ 𝑣 → ∃𝑔 ∈ 𝐿 (𝐺 “ 𝑔) ⊆ 𝑣))))) | 
| 158 | 135, 152,
157 | 3bitr4d 311 | 1
⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)))) |