Step | Hyp | Ref
| Expression |
1 | | fmucnd.1 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) |
2 | | fmucnd.4 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈)) |
3 | | cfilufbas 23641 |
. . . 4
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋)) |
4 | 1, 2, 3 | syl2anc 584 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋)) |
5 | | fmucnd.2 |
. . . 4
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) |
6 | | fmucnd.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) |
7 | | isucn 23630 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
8 | 7 | simprbda 499 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌) |
9 | 1, 5, 6, 8 | syl21anc 836 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
10 | 5 | elfvexd 6881 |
. . 3
⊢ (𝜑 → 𝑌 ∈ V) |
11 | | fmucnd.5 |
. . . 4
⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) |
12 | 11 | fbasrn 23235 |
. . 3
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌)) |
13 | 4, 9, 10, 12 | syl3anc 1371 |
. 2
⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌)) |
14 | | simplr 767 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ∈ 𝐶) |
15 | | eqid 2736 |
. . . . . . . 8
⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎) |
16 | | imaeq2 6009 |
. . . . . . . . 9
⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎)) |
17 | 16 | rspceeqv 3595 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
18 | 14, 15, 17 | sylancl 586 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
19 | | imaexg 7852 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V) |
20 | | eqid 2736 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
21 | 20 | elrnmpt 5911 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
22 | 6, 19, 21 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
23 | 22 | ad3antrrr 728 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
24 | 18, 23 | mpbird 256 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))) |
25 | | imaeq2 6009 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
26 | 25 | cbvmptv 5218 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
27 | 26 | rneqi 5892 |
. . . . . . 7
⊢ ran
(𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
28 | 11, 27 | eqtri 2764 |
. . . . . 6
⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
29 | 24, 28 | eleqtrrdi 2849 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷) |
30 | 9 | ffnd 6669 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
31 | 30 | ad3antrrr 728 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝐹 Fn 𝑋) |
32 | | fbelss 23184 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) |
33 | 4, 32 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) |
34 | 33 | ad4ant13 749 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ⊆ 𝑋) |
35 | | fmucndlem 23643 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
36 | 31, 34, 35 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
37 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
38 | 37 | mpofun 7480 |
. . . . . . . 8
⊢ Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
39 | | funimass2 6584 |
. . . . . . . 8
⊢ ((Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
40 | 38, 39 | mpan 688 |
. . . . . . 7
⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
41 | 40 | adantl 482 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
42 | 36, 41 | eqsstrrd 3983 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) |
43 | | id 22 |
. . . . . . . 8
⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎)) |
44 | 43 | sqxpeqd 5665 |
. . . . . . 7
⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
45 | 44 | sseq1d 3975 |
. . . . . 6
⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)) |
46 | 45 | rspcev 3581 |
. . . . 5
⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
47 | 29, 42, 46 | syl2anc 584 |
. . . 4
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
48 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋)) |
49 | 2 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈)) |
50 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌)) |
51 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉)) |
52 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
53 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑠〈(𝐹‘𝑥), (𝐹‘𝑦)〉 |
54 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑡〈(𝐹‘𝑥), (𝐹‘𝑦)〉 |
55 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥〈(𝐹‘𝑠), (𝐹‘𝑡)〉 |
56 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦〈(𝐹‘𝑠), (𝐹‘𝑡)〉 |
57 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠) |
58 | 57 | fveq2d 6846 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠)) |
59 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡) |
60 | 59 | fveq2d 6846 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡)) |
61 | 58, 60 | opeq12d 4838 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) |
62 | 53, 54, 55, 56, 61 | cbvmpo 7451 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) |
63 | 48, 50, 51, 52, 62 | ucnprima 23634 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) |
64 | | cfiluexsm 23642 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) |
65 | 48, 49, 63, 64 | syl3anc 1371 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) |
66 | 47, 65 | r19.29a 3159 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
67 | 66 | ralrimiva 3143 |
. 2
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
68 | | iscfilu 23640 |
. . 3
⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) |
69 | 5, 68 | syl 17 |
. 2
⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) |
70 | 13, 67, 69 | mpbir2and 711 |
1
⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉)) |