mposn

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

	Ref	Expression
Hypotheses	mposn.f	⊢ 𝐹 = ( 𝑥 ∈ { 𝐴 } , 𝑦 ∈ { 𝐵 } ↦ 𝐶 )
	mposn.a	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
	mposn.b	⊢ ( 𝑦 = 𝐵 → 𝐷 = 𝐸 )
Assertion	mposn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → 𝐹 = { ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐸 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		mposn.f	⊢ 𝐹 = ( 𝑥 ∈ { 𝐴 } , 𝑦 ∈ { 𝐵 } ↦ 𝐶 )
2		mposn.a	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
3		mposn.b	⊢ ( 𝑦 = 𝐵 → 𝐷 = 𝐸 )
4		xpsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
5	4	3adant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
6	5	mpteq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ( 𝑝 ∈ ( { 𝐴 } × { 𝐵 } ) ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑝 ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 ) )
7		mpompts	⊢ ( 𝑥 ∈ { 𝐴 } , 𝑦 ∈ { 𝐵 } ↦ 𝐶 ) = ( 𝑝 ∈ ( { 𝐴 } × { 𝐵 } ) ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 )
8	1 7	eqtri	⊢ 𝐹 = ( 𝑝 ∈ ( { 𝐴 } × { 𝐵 } ) ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 )
9	8	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → 𝐹 = ( 𝑝 ∈ ( { 𝐴 } × { 𝐵 } ) ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 ) )
10		op2ndg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 )
11		fveq2	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
12	11	eqcomd	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 2^nd ‘ 𝑝 ) )
13	12	eqeq1d	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 2^nd ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐵 ↔ ( 2^nd ‘ 𝑝 ) = 𝐵 ) )
14	10 13	syl5ibcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝐵 ) )
15	14	3adant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 2^nd ‘ 𝑝 ) = 𝐵 ) )
16	15	imp	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 2^nd ‘ 𝑝 ) = 𝐵 )
17		op1stg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 )
18		fveq2	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1^st ‘ 𝑝 ) = ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
19	18	eqcomd	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 1^st ‘ 𝑝 ) )
20	19	eqeq1d	⊢ ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( ( 1^st ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = 𝐴 ↔ ( 1^st ‘ 𝑝 ) = 𝐴 ) )
21	17 20	syl5ibcom	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1^st ‘ 𝑝 ) = 𝐴 ) )
22	21	3adant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ( 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ → ( 1^st ‘ 𝑝 ) = 𝐴 ) )
23	22	imp	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( 1^st ‘ 𝑝 ) = 𝐴 )
24		simp1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → 𝐴 ∈ 𝑉 )
25		simpl2	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑥 = 𝐴 ) → 𝐵 ∈ 𝑊 )
26	2	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐷 )
27	26 3	sylan9eq	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑥 = 𝐴 ) ∧ 𝑦 = 𝐵 ) → 𝐶 = 𝐸 )
28	25 27	csbied	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑥 = 𝐴 ) → ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐸 )
29	24 28	csbied	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐸 )
30	29	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐸 )
31		csbeq1	⊢ ( ( 1^st ‘ 𝑝 ) = 𝐴 → ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 )
32	31	eqeq1d	⊢ ( ( 1^st ‘ 𝑝 ) = 𝐴 → ( ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ) )
33	32	adantl	⊢ ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ( ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ) )
34		csbeq1	⊢ ( ( 2^nd ‘ 𝑝 ) = 𝐵 → ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
35	34	adantr	⊢ ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
36	35	csbeq2dv	⊢ ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
37	36	eqeq1d	⊢ ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ( ⦋ 𝐴 / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐸 ) )
38	33 37	bitrd	⊢ ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ( ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ↔ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = 𝐸 ) )
39	30 38	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) → ( ( ( 2^nd ‘ 𝑝 ) = 𝐵 ∧ ( 1^st ‘ 𝑝 ) = 𝐴 ) → ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 ) )
40	16 23 39	mp2and	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) ∧ 𝑝 = ⟨ 𝐴 , 𝐵 ⟩ ) → ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 = 𝐸 )
41		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
42	41	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ V )
43		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → 𝐸 ∈ 𝑈 )
44	40 42 43	fmptsnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → { ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐸 ⟩ } = ( 𝑝 ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑦 ⦌ 𝐶 ) )
45	6 9 44	3eqtr4d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐸 ∈ 𝑈 ) → 𝐹 = { ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐸 ⟩ } )

Metamath Proof Explorer

Theorem mposn

Proof