Step | Hyp | Ref
| Expression |
1 | | fmucnd.1 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) |
2 | | fmucnd.4 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (CauFilu‘𝑈)) |
3 | | cfilufbas 22093 |
. . . 4
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈)) → 𝐶 ∈ (fBas‘𝑋)) |
4 | 1, 2, 3 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (fBas‘𝑋)) |
5 | | fmucnd.2 |
. . . 4
⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) |
6 | | fmucnd.3 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) |
7 | | isucn 22082 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑣 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝐹‘𝑥)𝑣(𝐹‘𝑦))))) |
8 | 7 | simprbda 653 |
. . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) ∧ 𝐹 ∈ (𝑈 Cnu𝑉)) → 𝐹:𝑋⟶𝑌) |
9 | 1, 5, 6, 8 | syl21anc 1325 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
10 | 5 | elfvexd 6222 |
. . 3
⊢ (𝜑 → 𝑌 ∈ V) |
11 | | fmucnd.5 |
. . . 4
⊢ 𝐷 = ran (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) |
12 | 11 | fbasrn 21688 |
. . 3
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ V) → 𝐷 ∈ (fBas‘𝑌)) |
13 | 4, 9, 10, 12 | syl3anc 1326 |
. 2
⊢ (𝜑 → 𝐷 ∈ (fBas‘𝑌)) |
14 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ∈ 𝐶) |
15 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐹 “ 𝑎) = (𝐹 “ 𝑎) |
16 | | imaeq2 5462 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑎 → (𝐹 “ 𝑐) = (𝐹 “ 𝑎)) |
17 | 16 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑐 = 𝑎 → ((𝐹 “ 𝑎) = (𝐹 “ 𝑐) ↔ (𝐹 “ 𝑎) = (𝐹 “ 𝑎))) |
18 | 17 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐶 ∧ (𝐹 “ 𝑎) = (𝐹 “ 𝑎)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
19 | 14, 15, 18 | sylancl 694 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
20 | | imaexg 7103 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑈 Cnu𝑉) → (𝐹 “ 𝑎) ∈ V) |
21 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
22 | 21 | elrnmpt 5372 |
. . . . . . . . 9
⊢ ((𝐹 “ 𝑎) ∈ V → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
23 | 6, 20, 22 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
24 | 23 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) ↔ ∃𝑐 ∈ 𝐶 (𝐹 “ 𝑎) = (𝐹 “ 𝑐))) |
25 | 19, 24 | mpbird 247 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐))) |
26 | | imaeq2 5462 |
. . . . . . . . 9
⊢ (𝑎 = 𝑐 → (𝐹 “ 𝑎) = (𝐹 “ 𝑐)) |
27 | 26 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
28 | 27 | rneqi 5352 |
. . . . . . 7
⊢ ran
(𝑎 ∈ 𝐶 ↦ (𝐹 “ 𝑎)) = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
29 | 11, 28 | eqtri 2644 |
. . . . . 6
⊢ 𝐷 = ran (𝑐 ∈ 𝐶 ↦ (𝐹 “ 𝑐)) |
30 | 25, 29 | syl6eleqr 2712 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → (𝐹 “ 𝑎) ∈ 𝐷) |
31 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋) |
32 | 9, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑋) |
33 | 32 | ad3antrrr 766 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝐹 Fn 𝑋) |
34 | | simplll 798 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝜑) |
35 | | fbelss 21637 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (fBas‘𝑋) ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) |
36 | 4, 35 | sylan 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → 𝑎 ⊆ 𝑋) |
37 | 34, 14, 36 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → 𝑎 ⊆ 𝑋) |
38 | | fmucndlem 22095 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
39 | 33, 37, 38 | syl2anc 693 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
40 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
41 | 40 | mpt2fun 6762 |
. . . . . . . 8
⊢ Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
42 | | funimass2 5972 |
. . . . . . . 8
⊢ ((Fun
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
43 | 41, 42 | mpan 706 |
. . . . . . 7
⊢ ((𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
44 | 43 | adantl 482 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝑎 × 𝑎)) ⊆ 𝑣) |
45 | 39, 44 | eqsstr3d 3640 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) |
46 | | id 22 |
. . . . . . . 8
⊢ (𝑏 = (𝐹 “ 𝑎) → 𝑏 = (𝐹 “ 𝑎)) |
47 | 46 | sqxpeqd 5141 |
. . . . . . 7
⊢ (𝑏 = (𝐹 “ 𝑎) → (𝑏 × 𝑏) = ((𝐹 “ 𝑎) × (𝐹 “ 𝑎))) |
48 | 47 | sseq1d 3632 |
. . . . . 6
⊢ (𝑏 = (𝐹 “ 𝑎) → ((𝑏 × 𝑏) ⊆ 𝑣 ↔ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣)) |
49 | 48 | rspcev 3309 |
. . . . 5
⊢ (((𝐹 “ 𝑎) ∈ 𝐷 ∧ ((𝐹 “ 𝑎) × (𝐹 “ 𝑎)) ⊆ 𝑣) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
50 | 30, 45, 49 | syl2anc 693 |
. . . 4
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝑉) ∧ 𝑎 ∈ 𝐶) ∧ (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
51 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑈 ∈ (UnifOn‘𝑋)) |
52 | 2 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐶 ∈ (CauFilu‘𝑈)) |
53 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑉 ∈ (UnifOn‘𝑌)) |
54 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝐹 ∈ (𝑈 Cnu𝑉)) |
55 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
56 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑠〈(𝐹‘𝑥), (𝐹‘𝑦)〉 |
57 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑡〈(𝐹‘𝑥), (𝐹‘𝑦)〉 |
58 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥〈(𝐹‘𝑠), (𝐹‘𝑡)〉 |
59 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦〈(𝐹‘𝑠), (𝐹‘𝑡)〉 |
60 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑥 = 𝑠) |
61 | 60 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑥) = (𝐹‘𝑠)) |
62 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 𝑦 = 𝑡) |
63 | 62 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → (𝐹‘𝑦) = (𝐹‘𝑡)) |
64 | 61, 63 | opeq12d 4410 |
. . . . . . 7
⊢ ((𝑥 = 𝑠 ∧ 𝑦 = 𝑡) → 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) |
65 | 56, 57, 58, 59, 64 | cbvmpt2 6734 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑠 ∈ 𝑋, 𝑡 ∈ 𝑋 ↦ 〈(𝐹‘𝑠), (𝐹‘𝑡)〉) |
66 | 51, 53, 54, 55, 65 | ucnprima 22086 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) |
67 | | cfiluexsm 22094 |
. . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐶 ∈ (CauFilu‘𝑈) ∧ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣) ∈ 𝑈) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) |
68 | 51, 52, 66, 67 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑎 ∈ 𝐶 (𝑎 × 𝑎) ⊆ (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ 𝑣)) |
69 | 50, 68 | r19.29a 3078 |
. . 3
⊢ ((𝜑 ∧ 𝑣 ∈ 𝑉) → ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
70 | 69 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣) |
71 | | iscfilu 22092 |
. . 3
⊢ (𝑉 ∈ (UnifOn‘𝑌) → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) |
72 | 5, 71 | syl 17 |
. 2
⊢ (𝜑 → (𝐷 ∈ (CauFilu‘𝑉) ↔ (𝐷 ∈ (fBas‘𝑌) ∧ ∀𝑣 ∈ 𝑉 ∃𝑏 ∈ 𝐷 (𝑏 × 𝑏) ⊆ 𝑣))) |
73 | 13, 70, 72 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐷 ∈ (CauFilu‘𝑉)) |