Metamath Proof Explorer

Theorem mposn

Description: An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses mposn.f ⊢ F = x ∈ A , y ∈ B ⟼ C
mposn.a ⊢ x = A → C = D
mposn.b ⊢ y = B → D = E
Assertion mposn ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → F = A B E

Proof

Step Hyp Ref Expression
1 mposn.f ⊢ F = x ∈ A , y ∈ B ⟼ C
2 mposn.a ⊢ x = A → C = D
3 mposn.b ⊢ y = B → D = E
4 xpsng ⊢ A ∈ V ∧ B ∈ W → A × B = A B
5 4 3adant3 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → A × B = A B
6 5 mpteq1d ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → p ∈ A × B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = p ∈ A B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
7 mpompts ⊢ x ∈ A , y ∈ B ⟼ C = p ∈ A × B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
8 1 7 eqtri ⊢ F = p ∈ A × B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
9 8 a1i ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → F = p ∈ A × B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
10 op2ndg ⊢ A ∈ V ∧ B ∈ W → 2 nd ⁡ A B = B
11 fveq2 ⊢ p = A B → 2 nd ⁡ p = 2 nd ⁡ A B
12 11 eqcomd ⊢ p = A B → 2 nd ⁡ A B = 2 nd ⁡ p
13 12 eqeq1d ⊢ p = A B → 2 nd ⁡ A B = B ↔ 2 nd ⁡ p = B
14 10 13 syl5ibcom ⊢ A ∈ V ∧ B ∈ W → p = A B → 2 nd ⁡ p = B
15 14 3adant3 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → p = A B → 2 nd ⁡ p = B
16 15 imp ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ p = A B → 2 nd ⁡ p = B
17 op1stg ⊢ A ∈ V ∧ B ∈ W → 1 st ⁡ A B = A
18 fveq2 ⊢ p = A B → 1 st ⁡ p = 1 st ⁡ A B
19 18 eqcomd ⊢ p = A B → 1 st ⁡ A B = 1 st ⁡ p
20 19 eqeq1d ⊢ p = A B → 1 st ⁡ A B = A ↔ 1 st ⁡ p = A
21 17 20 syl5ibcom ⊢ A ∈ V ∧ B ∈ W → p = A B → 1 st ⁡ p = A
22 21 3adant3 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → p = A B → 1 st ⁡ p = A
23 22 imp ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ p = A B → 1 st ⁡ p = A
24 simp1 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → A ∈ V
25 simpl2 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ x = A → B ∈ W
26 2 adantl ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ x = A → C = D
27 26 3 sylan9eq ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ x = A ∧ y = B → C = E
28 25 27 csbied ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ x = A → ⦋ B / y⦌ C = E
29 24 28 csbied ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → ⦋ A / x⦌ ⦋ B / y⦌ C = E
30 29 adantr ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ p = A B → ⦋ A / x⦌ ⦋ B / y⦌ C = E
31 csbeq1 ⊢ 1 st ⁡ p = A → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = ⦋ A / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
32 31 eqeq1d ⊢ 1 st ⁡ p = A → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E ↔ ⦋ A / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E
33 32 adantl ⊢ 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E ↔ ⦋ A / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E
34 csbeq1 ⊢ 2 nd ⁡ p = B → ⦋ 2 nd ⁡ p / y⦌ C = ⦋ B / y⦌ C
35 34 adantr ⊢ 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ 2 nd ⁡ p / y⦌ C = ⦋ B / y⦌ C
36 35 csbeq2dv ⊢ 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ A / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = ⦋ A / x⦌ ⦋ B / y⦌ C
37 36 eqeq1d ⊢ 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ A / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E ↔ ⦋ A / x⦌ ⦋ B / y⦌ C = E
38 33 37 bitrd ⊢ 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E ↔ ⦋ A / x⦌ ⦋ B / y⦌ C = E
39 30 38 syl5ibrcom ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ p = A B → 2 nd ⁡ p = B ∧ 1 st ⁡ p = A → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E
40 16 23 39 mp2and ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U ∧ p = A B → ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C = E
41 opex ⊢ A B ∈ V
42 41 a1i ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → A B ∈ V
43 simp3 ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → E ∈ U
44 40 42 43 fmptsnd ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → A B E = p ∈ A B ⟼ ⦋ 1 st ⁡ p / x⦌ ⦋ 2 nd ⁡ p / y⦌ C
45 6 9 44 3eqtr4d ⊢ A ∈ V ∧ B ∈ W ∧ E ∈ U → F = A B E