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 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → 𝑝 ∈ ( 𝑋 × 𝑋 ) )
24 elxp2 ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
27 26 eleq1d ⊢ ( ( 𝜑 ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ) )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 ) )
29 df-br ⊢ ( 𝑥 𝑟 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑟 )
30 28 29 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑝 ∈ 𝑟 ↔ 𝑥 𝑟 𝑦 ) )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 ∈ ( 𝑋 × 𝑋 ) )
32 opex ⊢ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ∈ V
33 1 2 3 4 5 ucnimalem ⊢ 𝐺 = ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ↦ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
34 33 fvmpt2 ⊢ ( ( 𝑝 ∈ ( 𝑋 × 𝑋 ) ∧ ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ ∈ V ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
35 31 32 34 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
36 simpr ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ )
37 1st2nd2 ⊢ ( 𝑝 ∈ ( 𝑋 × 𝑋 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
38 31 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
39 36 38 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
40 vex ⊢ 𝑥 ∈ V
41 vex ⊢ 𝑦 ∈ V
42 40 41 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ↔ ( 𝑥 = ( 1st ‘ 𝑝 ) ∧ 𝑦 = ( 2nd ‘ 𝑝 ) ) )
43 39 42 sylib ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 = ( 1st ‘ 𝑝 ) ∧ 𝑦 = ( 2nd ‘ 𝑝 ) ) )
44 43 simpld ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 = ( 1st ‘ 𝑝 ) )
45 44 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) )
46 43 simprd ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 = ( 2nd ‘ 𝑝 ) )
47 46 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) )
48 45 47 opeq12d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ ( 1st ‘ 𝑝 ) ) , ( 𝐹 ‘ ( 2nd ‘ 𝑝 ) ) ⟩ )
49 35 48 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐺 ‘ 𝑝 ) = ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
50 49 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ 𝑊 ) )
51 df-br ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ 𝑊 )
52 50 51 bitr4di ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ↔ ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) )
53 30 52 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ↔ ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) )
54 53 exbiri ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
55 54 reximdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
56 55 reximdv ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
57 25 56 mpd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) )
58 57 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) )
59 22 58 r19.29d2r ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) )
60 pm3.35 ⊢ ( ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
61 60 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
62 61 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ∧ ( ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
63 59 62 syl ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) → ( 𝑝 ∈ 𝑟 → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
64 63 imp ⊢ ( ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ ( 𝑋 × 𝑋 ) ) ∧ 𝑝 ∈ 𝑟 ) → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
65 15 16 20 21 64 syl1111anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) ∧ 𝑝 ∈ 𝑟 ) → ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
66 65 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
67 66 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
68 67 reximdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑊 ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
69 14 68 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 )
70 5 mpofun ⊢ Fun 𝐺
71 opex ⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ V
72 5 71 dmmpo ⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
73 18 72 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ dom 𝐺 )
74 funimass4 ⊢ ( ( Fun 𝐺 ∧ 𝑟 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
75 70 73 74 sylancr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ) )
76 75 biimprd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) )
77 76 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) )
78 r19.29r ⊢ ( ( ∃ 𝑟 ∈ 𝑈 ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ∀ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) )
79 69 77 78 syl2anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) )
80 pm3.35 ⊢ ( ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )
81 80 reximi ⊢ ( ∃ 𝑟 ∈ 𝑈 ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 ∧ ( ∀ 𝑝 ∈ 𝑟 ( 𝐺 ‘ 𝑝 ) ∈ 𝑊 → ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ) ) → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )
82 79 81 syl ⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )