| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fmucnd.1 | . . . 4
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 2 |  | fmucnd.4 | . . . 4
⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈)) | 
| 3 |  | cfilufbas 24298 | . . . 4
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋)) | 
| 4 | 1, 2, 3 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋)) | 
| 5 |  | fmucnd.2 | . . . 4
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) | 
| 6 |  | fmucnd.3 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) | 
| 7 |  | isucn 24287 | . . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) | 
| 8 | 7 | simprbda 498 | . . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌) | 
| 9 | 1, 5, 6, 8 | syl21anc 838 | . . 3
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) | 
| 10 | 5 | elfvexd 6945 | . . 3
⊢ (𝜑 → 𝑌 ∈ V) | 
| 11 |  | fmucnd.5 | . . . 4
⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) | 
| 12 | 11 | fbasrn 23892 | . . 3
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌)) | 
| 13 | 4, 9, 10, 12 | syl3anc 1373 | . 2
⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌)) | 
| 14 |  | simplr 769 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ∈ 𝐶) | 
| 15 |  | eqid 2737 | . . . . . . . 8
⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎) | 
| 16 |  | imaeq2 6074 | . . . . . . . . 9
⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎)) | 
| 17 | 16 | rspceeqv 3645 | . . . . . . . 8
⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) | 
| 18 | 14, 15, 17 | sylancl 586 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) | 
| 19 |  | imaexg 7935 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V) | 
| 20 |  | eqid 2737 | . . . . . . . . . 10
⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) | 
| 21 | 20 | elrnmpt 5969 | . . . . . . . . 9
⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) | 
| 22 | 6, 19, 21 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) | 
| 23 | 22 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) | 
| 24 | 18, 23 | mpbird 257 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))) | 
| 25 |  | imaeq2 6074 | . . . . . . . . 9
⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) | 
| 26 | 25 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) | 
| 27 | 26 | rneqi 5948 | . . . . . . 7
⊢ ran
(𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) | 
| 28 | 11, 27 | eqtri 2765 | . . . . . 6
⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) | 
| 29 | 24, 28 | eleqtrrdi 2852 | . . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷) | 
| 30 | 9 | ffnd 6737 | . . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) | 
| 31 | 30 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝐹 Fn 𝑋) | 
| 32 |  | fbelss 23841 | . . . . . . . . 9
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) | 
| 33 | 4, 32 | sylan 580 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) | 
| 34 | 33 | ad4ant13 751 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ⊆ 𝑋) | 
| 35 |  | fmucndlem 24300 | . . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) | 
| 36 | 31, 34, 35 | syl2anc 584 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) | 
| 37 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 38 | 37 | mpofun 7557 | . . . . . . . 8
⊢ Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 39 |  | funimass2 6649 | . . . . . . . 8
⊢ ((Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) | 
| 40 | 38, 39 | mpan 690 | . . . . . . 7
⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) | 
| 41 | 40 | adantl 481 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) | 
| 42 | 36, 41 | eqsstrrd 4019 | . . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) | 
| 43 |  | id 22 | . . . . . . . 8
⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎)) | 
| 44 | 43 | sqxpeqd 5717 | . . . . . . 7
⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) | 
| 45 | 44 | sseq1d 4015 | . . . . . 6
⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)) | 
| 46 | 45 | rspcev 3622 | . . . . 5
⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) | 
| 47 | 29, 42, 46 | syl2anc 584 | . . . 4
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) | 
| 48 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 49 | 2 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈)) | 
| 50 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌)) | 
| 51 | 6 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉)) | 
| 52 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) | 
| 53 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑠〈(𝐹‘𝑥), (𝐹‘𝑦)〉 | 
| 54 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑡〈(𝐹‘𝑥), (𝐹‘𝑦)〉 | 
| 55 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑥〈(𝐹‘𝑠), (𝐹‘𝑡)〉 | 
| 56 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑦〈(𝐹‘𝑠), (𝐹‘𝑡)〉 | 
| 57 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠) | 
| 58 | 57 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠)) | 
| 59 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡) | 
| 60 | 59 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡)) | 
| 61 | 58, 60 | opeq12d 4881 | . . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) | 
| 62 | 53, 54, 55, 56, 61 | cbvmpo 7527 | . . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) | 
| 63 | 48, 50, 51, 52, 62 | ucnprima 24291 | . . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) | 
| 64 |  | cfiluexsm 24299 | . . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) | 
| 65 | 48, 49, 63, 64 | syl3anc 1373 | . . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) | 
| 66 | 47, 65 | r19.29a 3162 | . . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) | 
| 67 | 66 | ralrimiva 3146 | . 2
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) | 
| 68 |  | iscfilu 24297 | . . 3
⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) | 
| 69 | 5, 68 | syl 17 | . 2
⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) | 
| 70 | 13, 67, 69 | mpbir2and 713 | 1
⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉)) |