Metamath Proof Explorer

Theorem fnmpoovd

Description: A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses fnmpoovd.m ⊢ φ → M Fn A × B
fnmpoovd.s ⊢ i = a ∧ j = b → D = C
fnmpoovd.d ⊢ φ ∧ i ∈ A ∧ j ∈ B → D ∈ U
fnmpoovd.c ⊢ φ ∧ a ∈ A ∧ b ∈ B → C ∈ V
Assertion fnmpoovd ⊢ φ → M = a ∈ A , b ∈ B ⟼ C ↔ ∀ i ∈ A ∀ j ∈ B i M j = D

Proof

Step Hyp Ref Expression
1 fnmpoovd.m ⊢ φ → M Fn A × B
2 fnmpoovd.s ⊢ i = a ∧ j = b → D = C
3 fnmpoovd.d ⊢ φ ∧ i ∈ A ∧ j ∈ B → D ∈ U
4 fnmpoovd.c ⊢ φ ∧ a ∈ A ∧ b ∈ B → C ∈ V
5 4 3expb ⊢ φ ∧ a ∈ A ∧ b ∈ B → C ∈ V
6 5 ralrimivva ⊢ φ → ∀ a ∈ A ∀ b ∈ B C ∈ V
7 eqid ⊢ a ∈ A , b ∈ B ⟼ C = a ∈ A , b ∈ B ⟼ C
8 7 fnmpo ⊢ ∀ a ∈ A ∀ b ∈ B C ∈ V → a ∈ A , b ∈ B ⟼ C Fn A × B
9 6 8 syl ⊢ φ → a ∈ A , b ∈ B ⟼ C Fn A × B
10 eqfnov2 ⊢ M Fn A × B ∧ a ∈ A , b ∈ B ⟼ C Fn A × B → M = a ∈ A , b ∈ B ⟼ C ↔ ∀ i ∈ A ∀ j ∈ B i M j = i a ∈ A , b ∈ B ⟼ C j
11 1 9 10 syl2anc ⊢ φ → M = a ∈ A , b ∈ B ⟼ C ↔ ∀ i ∈ A ∀ j ∈ B i M j = i a ∈ A , b ∈ B ⟼ C j
12 nfcv ⊢ Ⅎ _ a D
13 nfcv ⊢ Ⅎ _ b D
14 nfcv ⊢ Ⅎ _ i C
15 nfcv ⊢ Ⅎ _ j C
16 12 13 14 15 2 cbvmpo ⊢ i ∈ A , j ∈ B ⟼ D = a ∈ A , b ∈ B ⟼ C
17 16 eqcomi ⊢ a ∈ A , b ∈ B ⟼ C = i ∈ A , j ∈ B ⟼ D
18 17 a1i ⊢ φ → a ∈ A , b ∈ B ⟼ C = i ∈ A , j ∈ B ⟼ D
19 18 oveqd ⊢ φ → i a ∈ A , b ∈ B ⟼ C j = i i ∈ A , j ∈ B ⟼ D j
20 19 eqeq2d ⊢ φ → i M j = i a ∈ A , b ∈ B ⟼ C j ↔ i M j = i i ∈ A , j ∈ B ⟼ D j
21 20 2ralbidv ⊢ φ → ∀ i ∈ A ∀ j ∈ B i M j = i a ∈ A , b ∈ B ⟼ C j ↔ ∀ i ∈ A ∀ j ∈ B i M j = i i ∈ A , j ∈ B ⟼ D j
22 simprl ⊢ φ ∧ i ∈ A ∧ j ∈ B → i ∈ A
23 simprr ⊢ φ ∧ i ∈ A ∧ j ∈ B → j ∈ B
24 3 3expb ⊢ φ ∧ i ∈ A ∧ j ∈ B → D ∈ U
25 eqid ⊢ i ∈ A , j ∈ B ⟼ D = i ∈ A , j ∈ B ⟼ D
26 25 ovmpt4g ⊢ i ∈ A ∧ j ∈ B ∧ D ∈ U → i i ∈ A , j ∈ B ⟼ D j = D
27 22 23 24 26 syl3anc ⊢ φ ∧ i ∈ A ∧ j ∈ B → i i ∈ A , j ∈ B ⟼ D j = D
28 27 eqeq2d ⊢ φ ∧ i ∈ A ∧ j ∈ B → i M j = i i ∈ A , j ∈ B ⟼ D j ↔ i M j = D
29 28 2ralbidva ⊢ φ → ∀ i ∈ A ∀ j ∈ B i M j = i i ∈ A , j ∈ B ⟼ D j ↔ ∀ i ∈ A ∀ j ∈ B i M j = D
30 11 21 29 3bitrd ⊢ φ → M = a ∈ A , b ∈ B ⟼ C ↔ ∀ i ∈ A ∀ j ∈ B i M j = D