Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ucnima Structured version   Visualization version   GIF version

Theorem ucnima 22132
 Description: An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
Hypotheses
Ref Expression
ucnprima.1 (𝜑𝑈 ∈ (UnifOn‘𝑋))
ucnprima.2 (𝜑𝑉 ∈ (UnifOn‘𝑌))
ucnprima.3 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
ucnprima.4 (𝜑𝑊𝑉)
ucnprima.5 𝐺 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
Assertion
Ref Expression
ucnima (𝜑 → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
Distinct variable groups:   𝑥,𝑦,𝐹   𝑥,𝑋,𝑦,𝑟   𝐹,𝑟   𝑥,𝐺,𝑦   𝑈,𝑟,𝑥,𝑦   𝑉,𝑟,𝑥   𝑊,𝑟,𝑥,𝑦   𝑋,𝑟   𝑌,𝑟,𝑥   𝜑,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐺(𝑟)   𝑉(𝑦)   𝑌(𝑦)

Proof of Theorem ucnima
Dummy variables 𝑝 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ucnprima.4 . . . . 5 (𝜑𝑊𝑉)
2 ucnprima.3 . . . . . . 7 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
3 ucnprima.1 . . . . . . . 8 (𝜑𝑈 ∈ (UnifOn‘𝑋))
4 ucnprima.2 . . . . . . . 8 (𝜑𝑉 ∈ (UnifOn‘𝑌))
5 isucn 22129 . . . . . . . 8 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
63, 4, 5syl2anc 694 . . . . . . 7 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
72, 6mpbid 222 . . . . . 6 (𝜑 → (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦))))
87simprd 478 . . . . 5 (𝜑 → ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))
9 breq 4687 . . . . . . . . 9 (𝑤 = 𝑊 → ((𝐹𝑥)𝑤(𝐹𝑦) ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
109imbi2d 329 . . . . . . . 8 (𝑤 = 𝑊 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
1110ralbidv 3015 . . . . . . 7 (𝑤 = 𝑊 → (∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
1211rexralbidv 3087 . . . . . 6 (𝑤 = 𝑊 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
1312rspcv 3336 . . . . 5 (𝑊𝑉 → (∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
141, 8, 13sylc 65 . . . 4 (𝜑 → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
15 simplll 813 . . . . . . . . 9 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝜑)
16 simplr 807 . . . . . . . . 9 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
1715, 16jca 553 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → (𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
18 ustssxp 22055 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
193, 18sylan 487 . . . . . . . . . 10 ((𝜑𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
2019sselda 3636 . . . . . . . . 9 (((𝜑𝑟𝑈) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
2120adantlr 751 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
22 simpr 476 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝𝑟)
23 simplr 807 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
24 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → 𝑝 ∈ (𝑋 × 𝑋))
25 elxp2 5166 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
2624, 25sylib 208 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
27 simpr 476 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
2827eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
2928adantlr 751 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
30 df-br 4686 . . . . . . . . . . . . . . . . . 18 (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
3129, 30syl6bbr 278 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟𝑥𝑟𝑦))
32 simplr 807 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 ∈ (𝑋 × 𝑋))
33 opex 4962 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V
34 ucnprima.5 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
353, 4, 2, 1, 34ucnimalem 22131 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3635fvmpt2 6330 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝑋 × 𝑋) ∧ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3732, 33, 36sylancl 695 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
38 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
39 1st2nd2 7249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ (𝑋 × 𝑋) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
4032, 39syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
4138, 40eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
42 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥 ∈ V
43 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
4442, 43opth 4974 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩ ↔ (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4541, 44sylib 208 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4645simpld 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑥 = (1st𝑝))
4746fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) = (𝐹‘(1st𝑝)))
4845simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑦 = (2nd𝑝))
4948fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) = (𝐹‘(2nd𝑝)))
5047, 49opeq12d 4441 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
5137, 50eqtr4d 2688 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5251eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊))
53 df-br 4686 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥)𝑊(𝐹𝑦) ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊)
5452, 53syl6bbr 278 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
5531, 54imbi12d 333 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑝𝑟 → (𝐺𝑝) ∈ 𝑊) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
5655exbiri 651 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5756reximdv 3045 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5857reximdv 3045 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5926, 58mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
6059adantlr 751 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
6123, 60r19.29d2r 3109 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
62 pm3.35 610 . . . . . . . . . . . 12 (((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6362rexlimivw 3058 . . . . . . . . . . 11 (∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6463rexlimivw 3058 . . . . . . . . . 10 (∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6561, 64syl 17 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6665imp 444 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6717, 21, 22, 66syl21anc 1365 . . . . . . 7 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6867ralrimiva 2995 . . . . . 6 (((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
6968ex 449 . . . . 5 ((𝜑𝑟𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7069reximdva 3046 . . . 4 (𝜑 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7114, 70mpd 15 . . 3 (𝜑 → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
7234mpt2fun 6804 . . . . . 6 Fun 𝐺
73 opex 4962 . . . . . . . 8 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
7434, 73dmmpt2 7285 . . . . . . 7 dom 𝐺 = (𝑋 × 𝑋)
7519, 74syl6sseqr 3685 . . . . . 6 ((𝜑𝑟𝑈) → 𝑟 ⊆ dom 𝐺)
76 funimass4 6286 . . . . . 6 ((Fun 𝐺𝑟 ⊆ dom 𝐺) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7772, 75, 76sylancr 696 . . . . 5 ((𝜑𝑟𝑈) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7877biimprd 238 . . . 4 ((𝜑𝑟𝑈) → (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
7978ralrimiva 2995 . . 3 (𝜑 → ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
80 r19.29r 3102 . . 3 ((∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
8171, 79, 80syl2anc 694 . 2 (𝜑 → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
82 pm3.35 610 . . 3 ((∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → (𝐺𝑟) ⊆ 𝑊)
8382reximi 3040 . 2 (∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
8481, 83syl 17 1 (𝜑 → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  Vcvv 3231   ⊆ wss 3607  ⟨cop 4216   class class class wbr 4685   × cxp 5141  dom cdm 5143   “ cima 5146  Fun wfun 5920  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1st c1st 7208  2nd c2nd 7209  UnifOncust 22050   Cnucucn 22126 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-ust 22051  df-ucn 22127 This theorem is referenced by:  ucnprima  22133
 Copyright terms: Public domain W3C validator