Metamath Proof Explorer

Theorem fmucndlem

Description: Lemma for fmucnd . (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion fmucndlem ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝐴 × 𝐴 ) ) = ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝐴 × 𝐴 ) ) = ran ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↾ ( 𝐴 × 𝐴 ) )
2 simpr ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
3 resmpo ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↾ ( 𝐴 × 𝐴 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) )
4 2 3 sylancom ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↾ ( 𝐴 × 𝐴 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) )
5 4 rneqd ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ran ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↾ ( 𝐴 × 𝐴 ) ) = ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) )
6 1 5 syl5eq ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝐴 × 𝐴 ) ) = ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) )
7 vex ⊢ 𝑥 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 op1std ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑝 ) = 𝑥 )
10 9 fveq2d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) = ( 𝐹 ‘ 𝑥 ) )
11 7 8 op2ndd ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑝 ) = 𝑦 )
12 11 fveq2d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) = ( 𝐹 ‘ 𝑦 ) )
13 10 12 opeq12d ⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
14 13 mpompt ⊢ ( 𝑝 ∈ ( 𝐴 × 𝐴 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
15 14 eqcomi ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ( 𝑝 ∈ ( 𝐴 × 𝐴 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
16 15 rneqi ⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ran ( 𝑝 ∈ ( 𝐴 × 𝐴 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
17 fvexd ⊢ ( ( ⊤ ∧ 𝑝 ∈ ( 𝐴 × 𝐴 ) ) → ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) ∈ V )
18 fvexd ⊢ ( ( ⊤ ∧ 𝑝 ∈ ( 𝐴 × 𝐴 ) ) → ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ∈ V )
19 16 17 18 fliftrel ⊢ ( ⊤ → ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ⊆ ( V × V ) )
20 19 mptru ⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ⊆ ( V × V )
21 20 sseli ⊢ ( 𝑝 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) → 𝑝 ∈ ( V × V ) )
22 21 adantl ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ) → 𝑝 ∈ ( V × V ) )
23 xpss ⊢ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ⊆ ( V × V )
24 23 sseli ⊢ ( 𝑝 ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) → 𝑝 ∈ ( V × V ) )
25 24 adantl ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ) → 𝑝 ∈ ( V × V ) )
26 eqid ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
27 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ V
28 26 27 elrnmpo ⊢ ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
29 eqcom ⊢ ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
30 fvex ⊢ ( 1st ‘ 𝑝 ) ∈ V
31 fvex ⊢ ( 2nd ‘ 𝑝 ) ∈ V
32 30 31 opth2 ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
33 29 32 bitri ⊢ ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
34 33 2rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
35 reeanv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
36 28 34 35 3bitri ⊢ ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
37 fvelimab ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 1st ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ) )
38 fvelimab ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 2nd ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) )
39 37 38 anbi12d ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( ( 1st ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 2nd ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 1st ‘ 𝑝 ) ∧ ∃ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 2nd ‘ 𝑝 ) ) ) )
40 36 39 bitr4id ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ( ( 1st ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 2nd ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ) ) )
41 opelxp ⊢ ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ↔ ( ( 1st ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ∧ ( 2nd ‘ 𝑝 ) ∈ ( 𝐹 “ 𝐴 ) ) )
42 40 41 bitr4di ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ) )
43 42 adantr ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( V × V ) ) → ( ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ) )
44 1st2nd2 ⊢ ( 𝑝 ∈ ( V × V ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
45 44 adantl ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( V × V ) ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
46 45 eleq1d ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( V × V ) ) → ( 𝑝 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ) )
47 45 eleq1d ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( V × V ) ) → ( 𝑝 ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ↔ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ) )
48 43 46 47 3bitr4d ⊢ ( ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑝 ∈ ( V × V ) ) → ( 𝑝 ∈ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ↔ 𝑝 ∈ ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) ) )
49 22 25 48 eqrdav ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) )
50 6 49 eqtrd ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝐴 × 𝐴 ) ) = ( ( 𝐹 “ 𝐴 ) × ( 𝐹 “ 𝐴 ) ) )