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

Theorem ucnima 23777
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 5149 . . . . . . . 8 (𝑤 = 𝑊 → ((𝐹𝑥)𝑤(𝐹𝑦) ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
21imbi2d 340 . . . . . . 7 (𝑤 = 𝑊 → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
32ralbidv 3177 . . . . . 6 (𝑤 = 𝑊 → (∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∀𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
43rexralbidv 3220 . . . . 5 (𝑤 = 𝑊 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)) ↔ ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
5 ucnprima.3 . . . . . . 7 (𝜑𝐹 ∈ (𝑈 Cnu𝑉))
6 ucnprima.1 . . . . . . . 8 (𝜑𝑈 ∈ (UnifOn‘𝑋))
7 ucnprima.2 . . . . . . . 8 (𝜑𝑉 ∈ (UnifOn‘𝑌))
8 isucn 23774 . . . . . . . 8 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
96, 7, 8syl2anc 584 . . . . . . 7 (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))))
105, 9mpbid 231 . . . . . 6 (𝜑 → (𝐹:𝑋𝑌 ∧ ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦))))
1110simprd 496 . . . . 5 (𝜑 → ∀𝑤𝑉𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑤(𝐹𝑦)))
12 ucnprima.4 . . . . 5 (𝜑𝑊𝑉)
134, 11, 12rspcdva 3613 . . . 4 (𝜑 → ∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
14 simplll 773 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝜑)
15 simplr 767 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
16 ustssxp 23700 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
176, 16sylan 580 . . . . . . . . . 10 ((𝜑𝑟𝑈) → 𝑟 ⊆ (𝑋 × 𝑋))
1817sselda 3981 . . . . . . . . 9 (((𝜑𝑟𝑈) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
1918adantlr 713 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝 ∈ (𝑋 × 𝑋))
20 simpr 485 . . . . . . . 8 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → 𝑝𝑟)
21 simplr 767 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)))
22 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → 𝑝 ∈ (𝑋 × 𝑋))
23 elxp2 5699 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝑋 × 𝑋) ↔ ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
2422, 23sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩)
25 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
2625eleq1d 2818 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
2726adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟))
28 df-br 5148 . . . . . . . . . . . . . . . . . 18 (𝑥𝑟𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑟)
2927, 28bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝𝑟𝑥𝑟𝑦))
30 simplr 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 ∈ (𝑋 × 𝑋))
31 opex 5463 . . . . . . . . . . . . . . . . . . . . 21 ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V
32 ucnprima.5 . . . . . . . . . . . . . . . . . . . . . . 23 𝐺 = (𝑥𝑋, 𝑦𝑋 ↦ ⟨(𝐹𝑥), (𝐹𝑦)⟩)
336, 7, 5, 12, 32ucnimalem 23776 . . . . . . . . . . . . . . . . . . . . . 22 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3433fvmpt2 7006 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝑋 × 𝑋) ∧ ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩ ∈ V) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
3530, 31, 34sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
36 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩)
37 1st2nd2 8010 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑝 ∈ (𝑋 × 𝑋) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
3830, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
3936, 38eqtr3d 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩)
40 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥 ∈ V
41 vex 3478 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 ∈ V
4240, 41opth 5475 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑦⟩ = ⟨(1st𝑝), (2nd𝑝)⟩ ↔ (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4339, 42sylib 217 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑥 = (1st𝑝) ∧ 𝑦 = (2nd𝑝)))
4443simpld 495 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑥 = (1st𝑝))
4544fveq2d 6892 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑥) = (𝐹‘(1st𝑝)))
4643simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑦 = (2nd𝑝))
4746fveq2d 6892 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐹𝑦) = (𝐹‘(2nd𝑝)))
4845, 47opeq12d 4880 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨(𝐹𝑥), (𝐹𝑦)⟩ = ⟨(𝐹‘(1st𝑝)), (𝐹‘(2nd𝑝))⟩)
4935, 48eqtr4d 2775 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → (𝐺𝑝) = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
5049eleq1d 2818 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊))
51 df-br 5148 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑥)𝑊(𝐹𝑦) ↔ ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ 𝑊)
5250, 51bitr4di 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝐺𝑝) ∈ 𝑊 ↔ (𝐹𝑥)𝑊(𝐹𝑦)))
5329, 52imbi12d 344 . . . . . . . . . . . . . . . 16 (((𝜑𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑝𝑟 → (𝐺𝑝) ∈ 𝑊) ↔ (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))))
5453exbiri 809 . . . . . . . . . . . . . . 15 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5554reximdv 3170 . . . . . . . . . . . . . 14 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5655reximdv 3170 . . . . . . . . . . . . 13 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → (∃𝑥𝑋𝑦𝑋 𝑝 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
5724, 56mpd 15 . . . . . . . . . . . 12 ((𝜑𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
5857adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊)))
5921, 58r19.29d2r 3140 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → ∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))))
60 pm3.35 801 . . . . . . . . . . . 12 (((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6160rexlimivw 3151 . . . . . . . . . . 11 (∃𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6261rexlimivw 3151 . . . . . . . . . 10 (∃𝑥𝑋𝑦𝑋 ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) ∧ ((𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6359, 62syl 17 . . . . . . . . 9 (((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) → (𝑝𝑟 → (𝐺𝑝) ∈ 𝑊))
6463imp 407 . . . . . . . 8 ((((𝜑 ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝 ∈ (𝑋 × 𝑋)) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6514, 15, 19, 20, 64syl1111anc 838 . . . . . . 7 ((((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) ∧ 𝑝𝑟) → (𝐺𝑝) ∈ 𝑊)
6665ralrimiva 3146 . . . . . 6 (((𝜑𝑟𝑈) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦))) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
6766ex 413 . . . . 5 ((𝜑𝑟𝑈) → (∀𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
6867reximdva 3168 . . . 4 (𝜑 → (∃𝑟𝑈𝑥𝑋𝑦𝑋 (𝑥𝑟𝑦 → (𝐹𝑥)𝑊(𝐹𝑦)) → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
6913, 68mpd 15 . . 3 (𝜑 → ∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊)
7032mpofun 7528 . . . . . 6 Fun 𝐺
71 opex 5463 . . . . . . . 8 ⟨(𝐹𝑥), (𝐹𝑦)⟩ ∈ V
7232, 71dmmpo 8053 . . . . . . 7 dom 𝐺 = (𝑋 × 𝑋)
7317, 72sseqtrrdi 4032 . . . . . 6 ((𝜑𝑟𝑈) → 𝑟 ⊆ dom 𝐺)
74 funimass4 6953 . . . . . 6 ((Fun 𝐺𝑟 ⊆ dom 𝐺) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7570, 73, 74sylancr 587 . . . . 5 ((𝜑𝑟𝑈) → ((𝐺𝑟) ⊆ 𝑊 ↔ ∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊))
7675biimprd 247 . . . 4 ((𝜑𝑟𝑈) → (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
7776ralrimiva 3146 . . 3 (𝜑 → ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊))
78 r19.29r 3116 . . 3 ((∃𝑟𝑈𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ ∀𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
7969, 77, 78syl2anc 584 . 2 (𝜑 → ∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)))
80 pm3.35 801 . . 3 ((∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → (𝐺𝑟) ⊆ 𝑊)
8180reximi 3084 . 2 (∃𝑟𝑈 (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 ∧ (∀𝑝𝑟 (𝐺𝑝) ∈ 𝑊 → (𝐺𝑟) ⊆ 𝑊)) → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
8279, 81syl 17 1 (𝜑 → ∃𝑟𝑈 (𝐺𝑟) ⊆ 𝑊)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  wrex 3070  Vcvv 3474  wss 3947  cop 4633   class class class wbr 5147   × cxp 5673  dom cdm 5675  cima 5678  Fun wfun 6534  wf 6536  cfv 6540  (class class class)co 7405  cmpo 7407  1st c1st 7969  2nd c2nd 7970  UnifOncust 23695   Cnucucn 23771
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 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-map 8818  df-ust 23696  df-ucn 23772
This theorem is referenced by:  ucnprima  23778
  Copyright terms: Public domain W3C validator