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

Theorem ustuqtop4 23756
Description: Lemma for ustuqtop 23758. (Contributed by Thierry Arnoux, 11-Jan-2018.)
Hypothesis
Ref Expression
utopustuq.1 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ π‘ˆ ↦ (𝑣 β€œ {𝑝})))
Assertion
Ref Expression
ustuqtop4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
Distinct variable groups:   𝑣,π‘ž,𝑝,π‘ˆ   𝑋,𝑝,π‘ž,𝑣   π‘Ž,𝑏,𝑝,π‘ž,𝑁   𝑣,π‘Ž,π‘ˆ,𝑏   𝑋,π‘Ž,𝑏
Allowed substitution hint:   𝑁(𝑣)

Proof of Theorem ustuqtop4
Dummy variables 𝑀 π‘Ÿ 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplll 773 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋))
2 simplr 767 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ 𝑒 ∈ π‘ˆ)
3 eqid 2732 . . . . . . . . . . 11 (𝑒 β€œ {𝑝}) = (𝑒 β€œ {𝑝})
4 imaeq1 6054 . . . . . . . . . . . 12 (𝑀 = 𝑒 β†’ (𝑀 β€œ {𝑝}) = (𝑒 β€œ {𝑝}))
54rspceeqv 3633 . . . . . . . . . . 11 ((𝑒 ∈ π‘ˆ ∧ (𝑒 β€œ {𝑝}) = (𝑒 β€œ {𝑝})) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
63, 5mpan2 689 . . . . . . . . . 10 (𝑒 ∈ π‘ˆ β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
76adantl 482 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
8 imaexg 7908 . . . . . . . . . 10 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {𝑝}) ∈ V)
9 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ π‘ˆ ↦ (𝑣 β€œ {𝑝})))
109ustuqtoplem 23751 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ (𝑒 β€œ {𝑝}) ∈ V) β†’ ((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝})))
118, 10sylan2 593 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ ((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝})))
127, 11mpbird 256 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘))
131, 2, 12syl2anc 584 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘))
14 simp-5l 783 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
151simpld 495 . . . . . . . . . . . . . 14 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
16 simp-4r 782 . . . . . . . . . . . . . 14 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ 𝑝 ∈ 𝑋)
17 ustimasn 23740 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ 𝑝 ∈ 𝑋) β†’ (𝑒 β€œ {𝑝}) βŠ† 𝑋)
1815, 2, 16, 17syl3anc 1371 . . . . . . . . . . . . 13 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (𝑒 β€œ {𝑝}) βŠ† 𝑋)
1918sselda 3982 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ π‘ž ∈ 𝑋)
2014, 19jca 512 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋))
21 simplr 767 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘ž ∈ (𝑒 β€œ {𝑝}))
22 simp-6l 785 . . . . . . . . . . . . . . . . . . 19 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
23 simp-4r 782 . . . . . . . . . . . . . . . . . . 19 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑒 ∈ π‘ˆ)
24 ustrel 23723 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ Rel 𝑒)
2522, 23, 24syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ Rel 𝑒)
26 elrelimasn 6084 . . . . . . . . . . . . . . . . . 18 (Rel 𝑒 β†’ (π‘ž ∈ (𝑒 β€œ {𝑝}) ↔ π‘π‘’π‘ž))
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘ž ∈ (𝑒 β€œ {𝑝}) ↔ π‘π‘’π‘ž))
2821, 27mpbid 231 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘π‘’π‘ž)
29 simpr 485 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘Ÿ ∈ (𝑒 β€œ {π‘ž}))
30 elrelimasn 6084 . . . . . . . . . . . . . . . . . 18 (Rel 𝑒 β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) ↔ π‘žπ‘’π‘Ÿ))
3125, 30syl 17 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) ↔ π‘žπ‘’π‘Ÿ))
3229, 31mpbid 231 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘žπ‘’π‘Ÿ)
33 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
34 vex 3478 . . . . . . . . . . . . . . . . . . 19 π‘Ÿ ∈ V
3533, 34brco 5870 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑒 ∘ 𝑒)π‘Ÿ ↔ βˆƒπ‘ž(π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ))
3635biimpri 227 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘ž(π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
373619.23bi 2184 . . . . . . . . . . . . . . . 16 ((π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
3828, 32, 37syl2anc 584 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
39 simpllr 774 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (𝑒 ∘ 𝑒) βŠ† 𝑀)
4039ssbrd 5191 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (𝑝(𝑒 ∘ 𝑒)π‘Ÿ β†’ π‘π‘€π‘Ÿ))
4138, 40mpd 15 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘π‘€π‘Ÿ)
42 simp-5r 784 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑀 ∈ π‘ˆ)
43 ustrel 23723 . . . . . . . . . . . . . . . 16 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ) β†’ Rel 𝑀)
4422, 42, 43syl2anc 584 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ Rel 𝑀)
45 elrelimasn 6084 . . . . . . . . . . . . . . 15 (Rel 𝑀 β†’ (π‘Ÿ ∈ (𝑀 β€œ {𝑝}) ↔ π‘π‘€π‘Ÿ))
4644, 45syl 17 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘Ÿ ∈ (𝑀 β€œ {𝑝}) ↔ π‘π‘€π‘Ÿ))
4741, 46mpbird 256 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘Ÿ ∈ (𝑀 β€œ {𝑝}))
4847ex 413 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) β†’ π‘Ÿ ∈ (𝑀 β€œ {𝑝})))
4948ssrdv 3988 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}))
50 simp-4r 782 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑀 ∈ π‘ˆ)
5116adantr 481 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑝 ∈ 𝑋)
52 ustimasn 23740 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ ∧ 𝑝 ∈ 𝑋) β†’ (𝑀 β€œ {𝑝}) βŠ† 𝑋)
5314, 50, 51, 52syl3anc 1371 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑀 β€œ {𝑝}) βŠ† 𝑋)
5420, 49, 533jca 1128 . . . . . . . . . 10 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋))
55 simpllr 774 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑒 ∈ π‘ˆ)
56 eqidd 2733 . . . . . . . . . . . . . 14 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž}))
57 imaeq1 6054 . . . . . . . . . . . . . . 15 (𝑀 = 𝑒 β†’ (𝑀 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž}))
5857rspceeqv 3633 . . . . . . . . . . . . . 14 ((𝑒 ∈ π‘ˆ ∧ (𝑒 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž})) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
5956, 58mpdan 685 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
6059adantl 482 . . . . . . . . . . . 12 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
61 imaexg 7908 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {π‘ž}) ∈ V)
629ustuqtoplem 23751 . . . . . . . . . . . . 13 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ V) β†’ ((𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž})))
6361, 62sylan2 593 . . . . . . . . . . . 12 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ ((𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž})))
6460, 63mpbird 256 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))
6514, 19, 55, 64syl21anc 836 . . . . . . . . . 10 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))
6654, 65jca 512 . . . . . . . . 9 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)))
67 imaexg 7908 . . . . . . . . . . 11 (𝑀 ∈ π‘ˆ β†’ (𝑀 β€œ {𝑝}) ∈ V)
68 sseq2 4008 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((𝑒 β€œ {π‘ž}) βŠ† 𝑏 ↔ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝})))
69 sseq1 4007 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (𝑏 βŠ† 𝑋 ↔ (𝑀 β€œ {𝑝}) βŠ† 𝑋))
7068, 693anbi23d 1439 . . . . . . . . . . . . . . 15 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋)))
7170anbi1d 630 . . . . . . . . . . . . . 14 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))))
7271anbi1d 630 . . . . . . . . . . . . 13 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ)))
73 eleq1 2821 . . . . . . . . . . . . 13 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (𝑏 ∈ (π‘β€˜π‘ž) ↔ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
7472, 73imbi12d 344 . . . . . . . . . . . 12 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑏 ∈ (π‘β€˜π‘ž)) ↔ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))))
75 sseq1 4007 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (π‘Ž βŠ† 𝑏 ↔ (𝑒 β€œ {π‘ž}) βŠ† 𝑏))
76753anbi2d 1441 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋)))
77 eleq1 2821 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (π‘Ž ∈ (π‘β€˜π‘ž) ↔ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)))
7876, 77anbi12d 631 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))))
7978imbi1d 341 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))))
80 eleq1 2821 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = π‘ž β†’ (𝑝 ∈ 𝑋 ↔ π‘ž ∈ 𝑋))
8180anbi2d 629 . . . . . . . . . . . . . . . . . . 19 (𝑝 = π‘ž β†’ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ↔ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋)))
82813anbi1d 1440 . . . . . . . . . . . . . . . . . 18 (𝑝 = π‘ž β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋)))
83 fveq2 6891 . . . . . . . . . . . . . . . . . . 19 (𝑝 = π‘ž β†’ (π‘β€˜π‘) = (π‘β€˜π‘ž))
8483eleq2d 2819 . . . . . . . . . . . . . . . . . 18 (𝑝 = π‘ž β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ π‘Ž ∈ (π‘β€˜π‘ž)))
8582, 84anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑝 = π‘ž β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž))))
8683eleq2d 2819 . . . . . . . . . . . . . . . . 17 (𝑝 = π‘ž β†’ (𝑏 ∈ (π‘β€˜π‘) ↔ 𝑏 ∈ (π‘β€˜π‘ž)))
8785, 86imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑝 = π‘ž β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ 𝑏 ∈ (π‘β€˜π‘)) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))))
889ustuqtop1 23753 . . . . . . . . . . . . . . . 16 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ 𝑏 ∈ (π‘β€˜π‘))
8987, 88chvarvv 2002 . . . . . . . . . . . . . . 15 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))
9079, 89vtoclg 3556 . . . . . . . . . . . . . 14 ((𝑒 β€œ {π‘ž}) ∈ V β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)))
9161, 90syl 17 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)))
9291impcom 408 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑏 ∈ (π‘β€˜π‘ž))
9374, 92vtoclg 3556 . . . . . . . . . . 11 ((𝑀 β€œ {𝑝}) ∈ V β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9467, 93syl 17 . . . . . . . . . 10 (𝑀 ∈ π‘ˆ β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9594impcom 408 . . . . . . . . 9 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
9666, 55, 50, 95syl21anc 836 . . . . . . . 8 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
9796ralrimiva 3146 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
98 raleq 3322 . . . . . . . 8 (𝑏 = (𝑒 β€œ {𝑝}) β†’ (βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž) ↔ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9998rspcev 3612 . . . . . . 7 (((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ∧ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
10013, 97, 99syl2anc 584 . . . . . 6 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
101 ustexhalf 23722 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘’ ∈ π‘ˆ (𝑒 ∘ 𝑒) βŠ† 𝑀)
102101adantlr 713 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘’ ∈ π‘ˆ (𝑒 ∘ 𝑒) βŠ† 𝑀)
103100, 102r19.29a 3162 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
104103adantr 481 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
105 eleq1 2821 . . . . . 6 (π‘Ž = (𝑀 β€œ {𝑝}) β†’ (π‘Ž ∈ (π‘β€˜π‘ž) ↔ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
106105rexralbidv 3220 . . . . 5 (π‘Ž = (𝑀 β€œ {𝑝}) β†’ (βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
107106adantl 482 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ (βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
108104, 107mpbird 256 . . 3 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
109108adantllr 717 . 2 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
110 vex 3478 . . . 4 π‘Ž ∈ V
1119ustuqtoplem 23751 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ V) β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝})))
112110, 111mpan2 689 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝})))
113112biimpa 477 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝}))
114109, 113r19.29a 3162 1 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   βŠ† wss 3948  {csn 4628   class class class wbr 5148   ↦ cmpt 5231  ran crn 5677   β€œ cima 5679   ∘ ccom 5680  Rel wrel 5681  β€˜cfv 6543  UnifOncust 23711
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-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ust 23712
This theorem is referenced by:  ustuqtop  23758  utopsnneiplem  23759
  Copyright terms: Public domain W3C validator