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

Theorem ucnima 23633
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 breq 5107 . . . . . . . 8 (𝑤 = 𝑊 → ((𝐹𝑥)𝑤(𝐹𝑦) ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
21imbi2d 340 . . . . . . 7 (𝑤 = 𝑊 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
32ralbidv 3174 . . . . . 6 (𝑤 = 𝑊 → (∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
43rexralbidv 3214 . . . . 5 (𝑤 = 𝑊 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
5 ucnprima.3 . . . . . . 7 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
6 ucnprima.1 . . . . . . . 8 (𝜑𝑈 ∈ (UnifOn‘𝑋))
7 ucnprima.2 . . . . . . . 8 (𝜑𝑉 ∈ (UnifOn‘𝑌))
8 isucn 23630 . . . . . . . 8 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
96, 7, 8syl2anc 584 . . . . . . 7 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
105, 9mpbid 231 . . . . . 6 (𝜑 → (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦))))
1110simprd 496 . . . . 5 (𝜑 → ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))
12 ucnprima.4 . . . . 5 (𝜑𝑊𝑉)
134, 11, 12rspcdva 3582 . . . 4 (𝜑 → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
14 simplll 773 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝜑)
15 simplr 767 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
16 ustssxp 23556 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
176, 16sylan 580 . . . . . . . . . 10 ((𝜑𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
1817sselda 3944 . . . . . . . . 9 (((𝜑𝑟𝑈) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
1918adantlr 713 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
20 simpr 485 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝𝑟)
21 simplr 767 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
22 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → 𝑝 ∈ (𝑋 × 𝑋))
23 elxp2 5657 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
2422, 23sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
25 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
2625eleq1d 2822 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
2726adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
28 df-br 5106 . . . . . . . . . . . . . . . . . 18 (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
2927, 28bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟𝑥𝑟𝑦))
30 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 ∈ (𝑋 × 𝑋))
31 opex 5421 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V
32 ucnprima.5 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
336, 7, 5, 12, 32ucnimalem 23632 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3433fvmpt2 6959 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝑋 × 𝑋) ∧ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3530, 31, 34sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
36 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
37 1st2nd2 7960 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ (𝑋 × 𝑋) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
3830, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
3936, 38eqtr3d 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
40 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥 ∈ V
41 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
4240, 41opth 5433 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩ ↔ (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4339, 42sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4443simpld 495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑥 = (1st𝑝))
4544fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) = (𝐹‘(1st𝑝)))
4643simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑦 = (2nd𝑝))
4746fveq2d 6846 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) = (𝐹‘(2nd𝑝)))
4845, 47opeq12d 4838 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
4935, 48eqtr4d 2779 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5049eleq1d 2822 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊))
51 df-br 5106 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥)𝑊(𝐹𝑦) ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊)
5250, 51bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
5329, 52imbi12d 344 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑝𝑟 → (𝐺𝑝) ∈ 𝑊) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
5453exbiri 809 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5554reximdv 3167 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5655reximdv 3167 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5724, 56mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
5857adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
5921, 58r19.29d2r 3137 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
60 pm3.35 801 . . . . . . . . . . . 12 (((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6160rexlimivw 3148 . . . . . . . . . . 11 (∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6261rexlimivw 3148 . . . . . . . . . 10 (∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6359, 62syl 17 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6463imp 407 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6514, 15, 19, 20, 64syl1111anc 838 . . . . . . 7 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6665ralrimiva 3143 . . . . . 6 (((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
6766ex 413 . . . . 5 ((𝜑𝑟𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
6867reximdva 3165 . . . 4 (𝜑 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
6913, 68mpd 15 . . 3 (𝜑 → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
7032mpofun 7480 . . . . . 6 Fun 𝐺
71 opex 5421 . . . . . . . 8 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
7232, 71dmmpo 8003 . . . . . . 7 dom 𝐺 = (𝑋 × 𝑋)
7317, 72sseqtrrdi 3995 . . . . . 6 ((𝜑𝑟𝑈) → 𝑟 ⊆ dom 𝐺)
74 funimass4 6907 . . . . . 6 ((Fun 𝐺𝑟 ⊆ dom 𝐺) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7570, 73, 74sylancr 587 . . . . 5 ((𝜑𝑟𝑈) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7675biimprd 247 . . . 4 ((𝜑𝑟𝑈) → (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
7776ralrimiva 3143 . . 3 (𝜑 → ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
78 r19.29r 3119 . . 3 ((∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
7969, 77, 78syl2anc 584 . 2 (𝜑 → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
80 pm3.35 801 . . 3 ((∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → (𝐺𝑟) ⊆ 𝑊)
8180reximi 3087 . 2 (∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
8279, 81syl 17 1 (𝜑 → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  wss 3910  cop 4592   class class class wbr 5105   × cxp 5631  dom cdm 5633  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920  UnifOncust 23551   Cnucucn 23627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-ust 23552  df-ucn 23628
This theorem is referenced by:  ucnprima  23634
  Copyright terms: Public domain W3C validator