Step | Hyp | Ref
| Expression |
1 | | df-ismty 35603 |
. . 3
⊢ Ismty =
(𝑚 ∈ ∪ ran ∞Met, 𝑛 ∈ ∪ ran
∞Met ↦ {𝑓
∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))}) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → Ismty = (𝑚 ∈ ∪ ran
∞Met, 𝑛 ∈ ∪ ran ∞Met ↦ {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))})) |
3 | | dmeq 5747 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → dom 𝑚 = dom 𝑀) |
4 | | xmetf 23085 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑀:(𝑋 × 𝑋)⟶ℝ*) |
5 | 4 | fdmd 6516 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (∞Met‘𝑋) → dom 𝑀 = (𝑋 × 𝑋)) |
6 | 3, 5 | sylan9eqr 2796 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑚 = 𝑀) → dom 𝑚 = (𝑋 × 𝑋)) |
7 | 6 | ad2ant2r 747 |
. . . . . . . 8
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom 𝑚 = (𝑋 × 𝑋)) |
8 | 7 | dmeqd 5749 |
. . . . . . 7
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom dom 𝑚 = dom (𝑋 × 𝑋)) |
9 | | dmxpid 5774 |
. . . . . . 7
⊢ dom
(𝑋 × 𝑋) = 𝑋 |
10 | 8, 9 | eqtrdi 2790 |
. . . . . 6
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom dom 𝑚 = 𝑋) |
11 | 10 | f1oeq2d 6617 |
. . . . 5
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ↔ 𝑓:𝑋–1-1-onto→dom
dom 𝑛)) |
12 | | dmeq 5747 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → dom 𝑛 = dom 𝑁) |
13 | | xmetf 23085 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑁:(𝑌 × 𝑌)⟶ℝ*) |
14 | 13 | fdmd 6516 |
. . . . . . . . . 10
⊢ (𝑁 ∈ (∞Met‘𝑌) → dom 𝑁 = (𝑌 × 𝑌)) |
15 | 12, 14 | sylan9eqr 2796 |
. . . . . . . . 9
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑛 = 𝑁) → dom 𝑛 = (𝑌 × 𝑌)) |
16 | 15 | ad2ant2l 746 |
. . . . . . . 8
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom 𝑛 = (𝑌 × 𝑌)) |
17 | 16 | dmeqd 5749 |
. . . . . . 7
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom dom 𝑛 = dom (𝑌 × 𝑌)) |
18 | | dmxpid 5774 |
. . . . . . 7
⊢ dom
(𝑌 × 𝑌) = 𝑌 |
19 | 17, 18 | eqtrdi 2790 |
. . . . . 6
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → dom dom 𝑛 = 𝑌) |
20 | | f1oeq3 6611 |
. . . . . 6
⊢ (dom dom
𝑛 = 𝑌 → (𝑓:𝑋–1-1-onto→dom
dom 𝑛 ↔ 𝑓:𝑋–1-1-onto→𝑌)) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → (𝑓:𝑋–1-1-onto→dom
dom 𝑛 ↔ 𝑓:𝑋–1-1-onto→𝑌)) |
22 | 11, 21 | bitrd 282 |
. . . 4
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ↔ 𝑓:𝑋–1-1-onto→𝑌)) |
23 | | oveq 7179 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (𝑥𝑚𝑦) = (𝑥𝑀𝑦)) |
24 | | oveq 7179 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦))) |
25 | 23, 24 | eqeqan12d 2756 |
. . . . . . 7
⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → ((𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) ↔ (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))) |
26 | 25 | adantl 485 |
. . . . . 6
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → ((𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) ↔ (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))) |
27 | 10, 26 | raleqbidv 3305 |
. . . . 5
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → (∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))) |
28 | 10, 27 | raleqbidv 3305 |
. . . 4
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → (∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))) |
29 | 22, 28 | anbi12d 634 |
. . 3
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → ((𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦))) ↔ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦))))) |
30 | 29 | abbidv 2803 |
. 2
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) ∧ (𝑚 = 𝑀 ∧ 𝑛 = 𝑁)) → {𝑓 ∣ (𝑓:dom dom 𝑚–1-1-onto→dom
dom 𝑛 ∧ ∀𝑥 ∈ dom dom 𝑚∀𝑦 ∈ dom dom 𝑚(𝑥𝑚𝑦) = ((𝑓‘𝑥)𝑛(𝑓‘𝑦)))} = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) |
31 | | fvssunirn 6706 |
. . 3
⊢
(∞Met‘𝑋)
⊆ ∪ ran ∞Met |
32 | | simpl 486 |
. . 3
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → 𝑀 ∈ (∞Met‘𝑋)) |
33 | 31, 32 | sseldi 3876 |
. 2
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → 𝑀 ∈ ∪ ran
∞Met) |
34 | | fvssunirn 6706 |
. . 3
⊢
(∞Met‘𝑌)
⊆ ∪ ran ∞Met |
35 | | simpr 488 |
. . 3
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → 𝑁 ∈ (∞Met‘𝑌)) |
36 | 34, 35 | sseldi 3876 |
. 2
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → 𝑁 ∈ ∪ ran
∞Met) |
37 | | f1of 6621 |
. . . . . 6
⊢ (𝑓:𝑋–1-1-onto→𝑌 → 𝑓:𝑋⟶𝑌) |
38 | 37 | adantr 484 |
. . . . 5
⊢ ((𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦))) → 𝑓:𝑋⟶𝑌) |
39 | | elfvdm 6709 |
. . . . . 6
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝑌 ∈ dom ∞Met) |
40 | | elfvdm 6709 |
. . . . . 6
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝑋 ∈ dom ∞Met) |
41 | | elmapg 8453 |
. . . . . 6
⊢ ((𝑌 ∈ dom ∞Met ∧
𝑋 ∈ dom ∞Met)
→ (𝑓 ∈ (𝑌 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝑌)) |
42 | 39, 40, 41 | syl2anr 600 |
. . . . 5
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑓 ∈ (𝑌 ↑m 𝑋) ↔ 𝑓:𝑋⟶𝑌)) |
43 | 38, 42 | syl5ibr 249 |
. . . 4
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → ((𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦))) → 𝑓 ∈ (𝑌 ↑m 𝑋))) |
44 | 43 | abssdv 3959 |
. . 3
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))} ⊆ (𝑌 ↑m 𝑋)) |
45 | | ovex 7206 |
. . . 4
⊢ (𝑌 ↑m 𝑋) ∈ V |
46 | 45 | ssex 5190 |
. . 3
⊢ ({𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))} ⊆ (𝑌 ↑m 𝑋) → {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))} ∈ V) |
47 | 44, 46 | syl 17 |
. 2
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))} ∈ V) |
48 | 2, 30, 33, 36, 47 | ovmpod 7320 |
1
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑁 ∈ (∞Met‘𝑌)) → (𝑀 Ismty 𝑁) = {𝑓 ∣ (𝑓:𝑋–1-1-onto→𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑀𝑦) = ((𝑓‘𝑥)𝑁(𝑓‘𝑦)))}) |