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

Theorem ustuqtop4 23970
Description: Lemma for ustuqtop 23972. (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 772 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋))
2 simplr 766 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ 𝑒 ∈ π‘ˆ)
3 eqid 2731 . . . . . . . . . . 11 (𝑒 β€œ {𝑝}) = (𝑒 β€œ {𝑝})
4 imaeq1 6055 . . . . . . . . . . . 12 (𝑀 = 𝑒 β†’ (𝑀 β€œ {𝑝}) = (𝑒 β€œ {𝑝}))
54rspceeqv 3634 . . . . . . . . . . 11 ((𝑒 ∈ π‘ˆ ∧ (𝑒 β€œ {𝑝}) = (𝑒 β€œ {𝑝})) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
63, 5mpan2 688 . . . . . . . . . 10 (𝑒 ∈ π‘ˆ β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
76adantl 481 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝}))
8 imaexg 7909 . . . . . . . . . 10 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {𝑝}) ∈ V)
9 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ π‘ˆ ↦ (𝑣 β€œ {𝑝})))
109ustuqtoplem 23965 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ (𝑒 β€œ {𝑝}) ∈ V) β†’ ((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝})))
118, 10sylan2 592 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ ((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {𝑝}) = (𝑀 β€œ {𝑝})))
127, 11mpbird 256 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘))
131, 2, 12syl2anc 583 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘))
14 simp-5l 782 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
151simpld 494 . . . . . . . . . . . . . 14 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
16 simp-4r 781 . . . . . . . . . . . . . 14 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ 𝑝 ∈ 𝑋)
17 ustimasn 23954 . . . . . . . . . . . . . 14 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ 𝑝 ∈ 𝑋) β†’ (𝑒 β€œ {𝑝}) βŠ† 𝑋)
1815, 2, 16, 17syl3anc 1370 . . . . . . . . . . . . 13 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ (𝑒 β€œ {𝑝}) βŠ† 𝑋)
1918sselda 3983 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ π‘ž ∈ 𝑋)
2014, 19jca 511 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋))
21 simplr 766 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘ž ∈ (𝑒 β€œ {𝑝}))
22 simp-6l 784 . . . . . . . . . . . . . . . . . . 19 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
23 simp-4r 781 . . . . . . . . . . . . . . . . . . 19 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑒 ∈ π‘ˆ)
24 ustrel 23937 . . . . . . . . . . . . . . . . . . 19 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ Rel 𝑒)
2522, 23, 24syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ Rel 𝑒)
26 elrelimasn 6085 . . . . . . . . . . . . . . . . . 18 (Rel 𝑒 β†’ (π‘ž ∈ (𝑒 β€œ {𝑝}) ↔ π‘π‘’π‘ž))
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘ž ∈ (𝑒 β€œ {𝑝}) ↔ π‘π‘’π‘ž))
2821, 27mpbid 231 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘π‘’π‘ž)
29 simpr 484 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘Ÿ ∈ (𝑒 β€œ {π‘ž}))
30 elrelimasn 6085 . . . . . . . . . . . . . . . . . 18 (Rel 𝑒 β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) ↔ π‘žπ‘’π‘Ÿ))
3125, 30syl 17 . . . . . . . . . . . . . . . . 17 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) ↔ π‘žπ‘’π‘Ÿ))
3229, 31mpbid 231 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘žπ‘’π‘Ÿ)
33 vex 3477 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
34 vex 3477 . . . . . . . . . . . . . . . . . . 19 π‘Ÿ ∈ V
3533, 34brco 5871 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑒 ∘ 𝑒)π‘Ÿ ↔ βˆƒπ‘ž(π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ))
3635biimpri 227 . . . . . . . . . . . . . . . . 17 (βˆƒπ‘ž(π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
373619.23bi 2183 . . . . . . . . . . . . . . . 16 ((π‘π‘’π‘ž ∧ π‘žπ‘’π‘Ÿ) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
3828, 32, 37syl2anc 583 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑝(𝑒 ∘ 𝑒)π‘Ÿ)
39 simpllr 773 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (𝑒 ∘ 𝑒) βŠ† 𝑀)
4039ssbrd 5192 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (𝑝(𝑒 ∘ 𝑒)π‘Ÿ β†’ π‘π‘€π‘Ÿ))
4138, 40mpd 15 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘π‘€π‘Ÿ)
42 simp-5r 783 . . . . . . . . . . . . . . . 16 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ 𝑀 ∈ π‘ˆ)
43 ustrel 23937 . . . . . . . . . . . . . . . 16 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ) β†’ Rel 𝑀)
4422, 42, 43syl2anc 583 . . . . . . . . . . . . . . 15 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ Rel 𝑀)
45 elrelimasn 6085 . . . . . . . . . . . . . . 15 (Rel 𝑀 β†’ (π‘Ÿ ∈ (𝑀 β€œ {𝑝}) ↔ π‘π‘€π‘Ÿ))
4644, 45syl 17 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ (π‘Ÿ ∈ (𝑀 β€œ {𝑝}) ↔ π‘π‘€π‘Ÿ))
4741, 46mpbird 256 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) ∧ π‘Ÿ ∈ (𝑒 β€œ {π‘ž})) β†’ π‘Ÿ ∈ (𝑀 β€œ {𝑝}))
4847ex 412 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (π‘Ÿ ∈ (𝑒 β€œ {π‘ž}) β†’ π‘Ÿ ∈ (𝑀 β€œ {𝑝})))
4948ssrdv 3989 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}))
50 simp-4r 781 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑀 ∈ π‘ˆ)
5116adantr 480 . . . . . . . . . . . 12 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑝 ∈ 𝑋)
52 ustimasn 23954 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ ∧ 𝑝 ∈ 𝑋) β†’ (𝑀 β€œ {𝑝}) βŠ† 𝑋)
5314, 50, 51, 52syl3anc 1370 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑀 β€œ {𝑝}) βŠ† 𝑋)
5420, 49, 533jca 1127 . . . . . . . . . 10 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋))
55 simpllr 773 . . . . . . . . . . 11 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ 𝑒 ∈ π‘ˆ)
56 eqidd 2732 . . . . . . . . . . . . . 14 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž}))
57 imaeq1 6055 . . . . . . . . . . . . . . 15 (𝑀 = 𝑒 β†’ (𝑀 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž}))
5857rspceeqv 3634 . . . . . . . . . . . . . 14 ((𝑒 ∈ π‘ˆ ∧ (𝑒 β€œ {π‘ž}) = (𝑒 β€œ {π‘ž})) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
5956, 58mpdan 684 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
6059adantl 481 . . . . . . . . . . . 12 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž}))
61 imaexg 7909 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ (𝑒 β€œ {π‘ž}) ∈ V)
629ustuqtoplem 23965 . . . . . . . . . . . . 13 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ V) β†’ ((𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž})))
6361, 62sylan2 592 . . . . . . . . . . . 12 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ ((𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘€ ∈ π‘ˆ (𝑒 β€œ {π‘ž}) = (𝑀 β€œ {π‘ž})))
6460, 63mpbird 256 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))
6514, 19, 55, 64syl21anc 835 . . . . . . . . . 10 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))
6654, 65jca 511 . . . . . . . . 9 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)))
67 imaexg 7909 . . . . . . . . . . 11 (𝑀 ∈ π‘ˆ β†’ (𝑀 β€œ {𝑝}) ∈ V)
68 sseq2 4009 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((𝑒 β€œ {π‘ž}) βŠ† 𝑏 ↔ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝})))
69 sseq1 4008 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (𝑏 βŠ† 𝑋 ↔ (𝑀 β€œ {𝑝}) βŠ† 𝑋))
7068, 693anbi23d 1438 . . . . . . . . . . . . . . 15 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋)))
7170anbi1d 629 . . . . . . . . . . . . . 14 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))))
7271anbi1d 629 . . . . . . . . . . . . 13 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ)))
73 eleq1 2820 . . . . . . . . . . . . 13 (𝑏 = (𝑀 β€œ {𝑝}) β†’ (𝑏 ∈ (π‘β€˜π‘ž) ↔ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
7472, 73imbi12d 343 . . . . . . . . . . . 12 (𝑏 = (𝑀 β€œ {𝑝}) β†’ ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑏 ∈ (π‘β€˜π‘ž)) ↔ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))))
75 sseq1 4008 . . . . . . . . . . . . . . . . . 18 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (π‘Ž βŠ† 𝑏 ↔ (𝑒 β€œ {π‘ž}) βŠ† 𝑏))
76753anbi2d 1440 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋)))
77 eleq1 2820 . . . . . . . . . . . . . . . . 17 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (π‘Ž ∈ (π‘β€˜π‘ž) ↔ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)))
7876, 77anbi12d 630 . . . . . . . . . . . . . . . 16 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž))))
7978imbi1d 340 . . . . . . . . . . . . . . 15 (π‘Ž = (𝑒 β€œ {π‘ž}) β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))))
80 eleq1 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = π‘ž β†’ (𝑝 ∈ 𝑋 ↔ π‘ž ∈ 𝑋))
8180anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑝 = π‘ž β†’ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ↔ (π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋)))
82813anbi1d 1439 . . . . . . . . . . . . . . . . . 18 (𝑝 = π‘ž β†’ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ↔ ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋)))
83 fveq2 6892 . . . . . . . . . . . . . . . . . . 19 (𝑝 = π‘ž β†’ (π‘β€˜π‘) = (π‘β€˜π‘ž))
8483eleq2d 2818 . . . . . . . . . . . . . . . . . 18 (𝑝 = π‘ž β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ π‘Ž ∈ (π‘β€˜π‘ž)))
8582, 84anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑝 = π‘ž β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) ↔ (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž))))
8683eleq2d 2818 . . . . . . . . . . . . . . . . 17 (𝑝 = π‘ž β†’ (𝑏 ∈ (π‘β€˜π‘) ↔ 𝑏 ∈ (π‘β€˜π‘ž)))
8785, 86imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑝 = π‘ž β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ 𝑏 ∈ (π‘β€˜π‘)) ↔ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))))
889ustuqtop1 23967 . . . . . . . . . . . . . . . 16 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ 𝑏 ∈ (π‘β€˜π‘))
8987, 88chvarvv 2001 . . . . . . . . . . . . . . 15 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ π‘Ž βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž))
9079, 89vtoclg 3557 . . . . . . . . . . . . . 14 ((𝑒 β€œ {π‘ž}) ∈ V β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)))
9161, 90syl 17 . . . . . . . . . . . . 13 (𝑒 ∈ π‘ˆ β†’ ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) β†’ 𝑏 ∈ (π‘β€˜π‘ž)))
9291impcom 407 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† 𝑏 ∧ 𝑏 βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑏 ∈ (π‘β€˜π‘ž))
9374, 92vtoclg 3557 . . . . . . . . . . 11 ((𝑀 β€œ {𝑝}) ∈ V β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9467, 93syl 17 . . . . . . . . . 10 (𝑀 ∈ π‘ˆ β†’ (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9594impcom 407 . . . . . . . . 9 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ π‘ž ∈ 𝑋) ∧ (𝑒 β€œ {π‘ž}) βŠ† (𝑀 β€œ {𝑝}) ∧ (𝑀 β€œ {𝑝}) βŠ† 𝑋) ∧ (𝑒 β€œ {π‘ž}) ∈ (π‘β€˜π‘ž)) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑀 ∈ π‘ˆ) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
9666, 55, 50, 95syl21anc 835 . . . . . . . 8 ((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) ∧ π‘ž ∈ (𝑒 β€œ {𝑝})) β†’ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
9796ralrimiva 3145 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
98 raleq 3321 . . . . . . . 8 (𝑏 = (𝑒 β€œ {𝑝}) β†’ (βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž) ↔ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
9998rspcev 3613 . . . . . . 7 (((𝑒 β€œ {𝑝}) ∈ (π‘β€˜π‘) ∧ βˆ€π‘ž ∈ (𝑒 β€œ {𝑝})(𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
10013, 97, 99syl2anc 583 . . . . . 6 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ 𝑒 ∈ π‘ˆ) ∧ (𝑒 ∘ 𝑒) βŠ† 𝑀) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
101 ustexhalf 23936 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘’ ∈ π‘ˆ (𝑒 ∘ 𝑒) βŠ† 𝑀)
102101adantlr 712 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘’ ∈ π‘ˆ (𝑒 ∘ 𝑒) βŠ† 𝑀)
103100, 102r19.29a 3161 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
104103adantr 480 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž))
105 eleq1 2820 . . . . . 6 (π‘Ž = (𝑀 β€œ {𝑝}) β†’ (π‘Ž ∈ (π‘β€˜π‘ž) ↔ (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
106105rexralbidv 3219 . . . . 5 (π‘Ž = (𝑀 β€œ {𝑝}) β†’ (βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
107106adantl 481 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ (βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž) ↔ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 (𝑀 β€œ {𝑝}) ∈ (π‘β€˜π‘ž)))
108104, 107mpbird 256 . . 3 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
109108adantllr 716 . 2 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) ∧ 𝑀 ∈ π‘ˆ) ∧ π‘Ž = (𝑀 β€œ {𝑝})) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
110 vex 3477 . . . 4 π‘Ž ∈ V
1119ustuqtoplem 23965 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ V) β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝})))
112110, 111mpan2 688 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) β†’ (π‘Ž ∈ (π‘β€˜π‘) ↔ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝})))
113112biimpa 476 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ βˆƒπ‘€ ∈ π‘ˆ π‘Ž = (𝑀 β€œ {𝑝}))
114109, 113r19.29a 3161 1 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑝 ∈ 𝑋) ∧ π‘Ž ∈ (π‘β€˜π‘)) β†’ βˆƒπ‘ ∈ (π‘β€˜π‘)βˆ€π‘ž ∈ 𝑏 π‘Ž ∈ (π‘β€˜π‘ž))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   βŠ† wss 3949  {csn 4629   class class class wbr 5149   ↦ cmpt 5232  ran crn 5678   β€œ cima 5680   ∘ ccom 5681  Rel wrel 5682  β€˜cfv 6544  UnifOncust 23925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ust 23926
This theorem is referenced by:  ustuqtop  23972  utopsnneiplem  23973
  Copyright terms: Public domain W3C validator