Metamath Proof Explorer

Theorem ucnima

Description: An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Hypotheses ucnprima.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
ucnprima.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
ucnprima.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
ucnprima.4 ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
ucnprima.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
Assertion ucnima ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )

Proof

Step Hyp Ref Expression
1 ucnprima.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 ucnprima.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3 ucnprima.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
4 ucnprima.4 ⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
5 ucnprima.5 ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
6 breq ⊢ ( 𝑤 = 𝑊 → ( ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
7 6 imbi2d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) )
8 7 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) )
9 8 rexralbidv ⊢ ( 𝑤 = 𝑊 → ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) )
10 isucn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ) ) )
11 1 2 10 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ) ) )
12 3 11 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑤 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) ) )
13 12 simprd ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑤 ( 𝐹 ‘ 𝑦 ) ) )
14 9 13 4 rspcdva ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
15 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → 𝜑 )
16 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
17 ustssxp ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
18 1 17 sylan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
19 18 sselda ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ 𝑝 ∈ 𝑟 ) → 𝑝 ∈ ( 𝑋 × 𝑋 ) )
20 19 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → 𝑝 ∈ ( 𝑋 × 𝑋 ) )
21 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → 𝑝 ∈ 𝑟 )
22 simplr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
23 elxp2 ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
24 23 bilani ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
26 25 eleq1d ⊢ ( ( 𝜑 ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ) )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ) )
28 df-br ⊢ ( 𝑥 𝑟 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 )
29 27 28 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ 𝑥 𝑟 𝑦 ) )
30 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 ∈ ( 𝑋 × 𝑋 ) )
31 opex ⊢ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ∈ V
32 1 2 3 4 5 ucnimalem ⊢ 𝐺 = ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
33 32 fvmpt2 ⊢ ( ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ∧ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ∈ V ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
34 30 31 33 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
35 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
36 1st2nd2 ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑋 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
37 30 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
38 35 37 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
39 vex ⊢ 𝑥 ∈ V
40 vex ⊢ 𝑦 ∈ V
41 39 40 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ↔ ( 𝑥 = ( 1st ‘ 𝑝 ) ∧ 𝑦 = ( 2nd ‘ 𝑝 ) ) )
42 38 41 sylib ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 = ( 1st ‘ 𝑝 ) ∧ 𝑦 = ( 2nd ‘ 𝑝 ) ) )
43 42 simpld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 = ( 1st ‘ 𝑝 ) )
44 43 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) )
45 42 simprd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 = ( 2nd ‘ 𝑝 ) )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) )
47 44 46 opeq12d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
48 34 47 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
49 48 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ 𝑊 ) )
50 df-br ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ 𝑊 )
51 49 50 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ↔ ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
52 29 51 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ↔ ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) )
53 52 exbiri ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
54 53 reximdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
55 54 reximdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
56 24 55 mpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) )
58 22 57 r19.29d2r ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
59 pm3.35 ⊢ ( ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
60 59 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
61 60 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
62 58 61 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
63 62 imp ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 ∈ 𝑟 ) → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
64 15 16 20 21 63 syl1111anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
65 64 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
66 65 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
67 66 reximdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
68 14 67 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
69 5 mpofun ⊢ Fun 𝐺
70 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ V
71 5 70 dmmpo ⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
72 18 71 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ dom 𝐺 )
73 funimass4 ⊢ ( ( Fun 𝐺 ∧ 𝑟 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
74 69 72 73 sylancr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
75 74 biimprd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) )
76 75 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) )
77 r19.29r ⊢ ( ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ∀ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) )
78 68 76 77 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) )
79 pm3.35 ⊢ ( ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )
80 79 reximi ⊢ ( ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )
81 78 80 syl ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )