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

Theorem ustuqtop4 22327
Description: Lemma for ustuqtop 22329. (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 791 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋))
2 simplr 785 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑢𝑈)
3 eqid 2765 . . . . . . . . . . 11 (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4 imaeq1 5643 . . . . . . . . . . . 12 (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
54rspceeqv 3479 . . . . . . . . . . 11 ((𝑢𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
63, 5mpan2 682 . . . . . . . . . 10 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
76adantl 473 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8 imaexg 7301 . . . . . . . . . 10 (𝑢𝑈 → (𝑢 “ {𝑝}) ∈ V)
9 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
109ustuqtoplem 22322 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
118, 10sylan2 586 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
127, 11mpbird 248 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
131, 2, 12syl2anc 579 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
14 simp-5l 805 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
151simpld 488 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
16 simp-4r 803 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑝𝑋)
17 ustimasn 22311 . . . . . . . . . . . . . 14 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑝𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1815, 2, 16, 17syl3anc 1490 . . . . . . . . . . . . 13 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1918sselda 3761 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞𝑋)
2014, 19jca 507 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋))
21 simplr 785 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
22 simp-6l 809 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
23 simp-4r 803 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢𝑈)
24 ustrel 22294 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → Rel 𝑢)
2522, 23, 24syl2anc 579 . . . . . . . . . . . . . . . . . 18 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
26 elrelimasn 5671 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2821, 27mpbid 223 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
29 simpr 477 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
30 elrelimasn 5671 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3125, 30syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3229, 31mpbid 223 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
33 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
34 vex 3353 . . . . . . . . . . . . . . . . . . 19 𝑟 ∈ V
3533, 34brco 5461 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑢𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟))
3635biimpri 219 . . . . . . . . . . . . . . . . 17 (∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
373619.23bi 2223 . . . . . . . . . . . . . . . 16 ((𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
3828, 32, 37syl2anc 579 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢𝑢)𝑟)
39 simpllr 793 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢𝑢) ⊆ 𝑤)
4039ssbrd 4852 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢𝑢)𝑟𝑝𝑤𝑟))
4138, 40mpd 15 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
42 simp-5r 807 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤𝑈)
43 ustrel 22294 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → Rel 𝑤)
4422, 42, 43syl2anc 579 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
45 elrelimasn 5671 . . . . . . . . . . . . . . 15 (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4644, 45syl 17 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4741, 46mpbird 248 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
4847ex 401 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
4948ssrdv 3767 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
50 simp-4r 803 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤𝑈)
5116adantr 472 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝𝑋)
52 ustimasn 22311 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈𝑝𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5314, 50, 51, 52syl3anc 1490 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5420, 49, 533jca 1158 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
55 simpllr 793 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢𝑈)
56 eqidd 2766 . . . . . . . . . . . . . 14 (𝑢𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
57 imaeq1 5643 . . . . . . . . . . . . . . 15 (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
5857rspceeqv 3479 . . . . . . . . . . . . . 14 ((𝑢𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
5956, 58mpdan 678 . . . . . . . . . . . . 13 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6059adantl 473 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61 imaexg 7301 . . . . . . . . . . . . 13 (𝑢𝑈 → (𝑢 “ {𝑞}) ∈ V)
629ustuqtoplem 22322 . . . . . . . . . . . . 13 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6361, 62sylan2 586 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6460, 63mpbird 248 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6514, 19, 55, 64syl21anc 866 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6654, 65jca 507 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
67 imaexg 7301 . . . . . . . . . . 11 (𝑤𝑈 → (𝑤 “ {𝑝}) ∈ V)
68 sseq2 3787 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
69 sseq1 3786 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → (𝑏𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
7068, 693anbi23d 1563 . . . . . . . . . . . . . . 15 (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
7170anbi1d 623 . . . . . . . . . . . . . 14 (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7271anbi1d 623 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈)))
73 eleq1 2832 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
7472, 73imbi12d 335 . . . . . . . . . . . 12 (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))))
75 sseq1 3786 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑢 “ {𝑞}) → (𝑎𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
76753anbi2d 1565 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋)))
77 eleq1 2832 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
7876, 77anbi12d 624 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7978imbi1d 332 . . . . . . . . . . . . . . 15 (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
80 eleq1 2832 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
8180anbi2d 622 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋)))
82813anbi1d 1564 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋)))
83 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
8483eleq2d 2830 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑞)))
8582, 84anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞))))
8683eleq2d 2830 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑞)))
8785, 86imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
889ustuqtop1 22324 . . . . . . . . . . . . . . . 16 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
8987, 88chvarv 2369 . . . . . . . . . . . . . . 15 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))
9079, 89vtoclg 3418 . . . . . . . . . . . . . 14 ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9161, 90syl 17 . . . . . . . . . . . . 13 (𝑢𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9291impcom 396 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞))
9374, 92vtoclg 3418 . . . . . . . . . . 11 ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9467, 93syl 17 . . . . . . . . . 10 (𝑤𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9594impcom 396 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ∧ 𝑤𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9666, 55, 50, 95syl21anc 866 . . . . . . . 8 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9796ralrimiva 3113 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞))
98 raleq 3286 . . . . . . . 8 (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9998rspcev 3461 . . . . . . 7 (((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
10013, 97, 99syl2anc 579 . . . . . 6 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
101 ustexhalf 22293 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
102101adantlr 706 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
103100, 102r19.29a 3225 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
104103adantr 472 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
105 eleq1 2832 . . . . . 6 (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
106105rexralbidv 3205 . . . . 5 (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
107106adantl 473 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
108104, 107mpbird 248 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
109108adantllr 710 . 2 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
110 vex 3353 . . . 4 𝑎 ∈ V
1119ustuqtoplem 22322 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
112110, 111mpan2 682 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
113112biimpa 468 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
114109, 113r19.29a 3225 1 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  wss 3732  {csn 4334   class class class wbr 4809  cmpt 4888  ran crn 5278  cima 5280  ccom 5281  Rel wrel 5282  cfv 6068  UnifOncust 22282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ust 22283
This theorem is referenced by:  ustuqtop  22329  utopsnneiplem  22330
  Copyright terms: Public domain W3C validator