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

Theorem ustuqtop4 23596
Description: Lemma for ustuqtop 23598. (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 2736 . . . . . . . . . . 11 (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4 imaeq1 6008 . . . . . . . . . . . 12 (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
54rspceeqv 3595 . . . . . . . . . . 11 ((𝑢𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
63, 5mpan2 689 . . . . . . . . . 10 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
76adantl 482 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
8 imaexg 7852 . . . . . . . . . 10 (𝑢𝑈 → (𝑢 “ {𝑝}) ∈ V)
9 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
109ustuqtoplem 23591 . . . . . . . . . 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 23580 . . . . . . . . . . . . . 14 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑝𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1815, 2, 16, 17syl3anc 1371 . . . . . . . . . . . . 13 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1918sselda 3944 . . . . . . . . . . . 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 23563 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → Rel 𝑢)
2522, 23, 24syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
26 elrelimasn 6037 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2725, 26syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2821, 27mpbid 231 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
29 simpr 485 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
30 elrelimasn 6037 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3125, 30syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3229, 31mpbid 231 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
33 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
34 vex 3449 . . . . . . . . . . . . . . . . . . 19 𝑟 ∈ V
3533, 34brco 5826 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑢𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟))
3635biimpri 227 . . . . . . . . . . . . . . . . 17 (∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
373619.23bi 2184 . . . . . . . . . . . . . . . 16 ((𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
3828, 32, 37syl2anc 584 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢𝑢)𝑟)
39 simpllr 774 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢𝑢) ⊆ 𝑤)
4039ssbrd 5148 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢𝑢)𝑟𝑝𝑤𝑟))
4138, 40mpd 15 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
42 simp-5r 784 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤𝑈)
43 ustrel 23563 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → Rel 𝑤)
4422, 42, 43syl2anc 584 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
45 elrelimasn 6037 . . . . . . . . . . . . . . 15 (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4644, 45syl 17 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4741, 46mpbird 256 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
4847ex 413 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
4948ssrdv 3950 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
50 simp-4r 782 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤𝑈)
5116adantr 481 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝𝑋)
52 ustimasn 23580 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈𝑝𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5314, 50, 51, 52syl3anc 1371 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5420, 49, 533jca 1128 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
55 simpllr 774 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢𝑈)
56 eqidd 2737 . . . . . . . . . . . . . 14 (𝑢𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
57 imaeq1 6008 . . . . . . . . . . . . . . 15 (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
5857rspceeqv 3595 . . . . . . . . . . . . . 14 ((𝑢𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
5956, 58mpdan 685 . . . . . . . . . . . . 13 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6059adantl 482 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
61 imaexg 7852 . . . . . . . . . . . . 13 (𝑢𝑈 → (𝑢 “ {𝑞}) ∈ V)
629ustuqtoplem 23591 . . . . . . . . . . . . 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 7852 . . . . . . . . . . 11 (𝑤𝑈 → (𝑤 “ {𝑝}) ∈ V)
68 sseq2 3970 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
69 sseq1 3969 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → (𝑏𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
7068, 693anbi23d 1439 . . . . . . . . . . . . . . 15 (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
7170anbi1d 630 . . . . . . . . . . . . . 14 (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7271anbi1d 630 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈)))
73 eleq1 2825 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
7472, 73imbi12d 344 . . . . . . . . . . . 12 (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))))
75 sseq1 3969 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑢 “ {𝑞}) → (𝑎𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
76753anbi2d 1441 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋)))
77 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
7876, 77anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7978imbi1d 341 . . . . . . . . . . . . . . 15 (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
80 eleq1 2825 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
8180anbi2d 629 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋)))
82813anbi1d 1440 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋)))
83 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
8483eleq2d 2823 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑞)))
8582, 84anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞))))
8683eleq2d 2823 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑞)))
8785, 86imbi12d 344 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
889ustuqtop1 23593 . . . . . . . . . . . . . . . 16 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
8987, 88chvarvv 2002 . . . . . . . . . . . . . . 15 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))
9079, 89vtoclg 3525 . . . . . . . . . . . . . 14 ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9161, 90syl 17 . . . . . . . . . . . . 13 (𝑢𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9291impcom 408 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞))
9374, 92vtoclg 3525 . . . . . . . . . . 11 ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9467, 93syl 17 . . . . . . . . . 10 (𝑤𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9594impcom 408 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ∧ 𝑤𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9666, 55, 50, 95syl21anc 836 . . . . . . . 8 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9796ralrimiva 3143 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞))
98 raleq 3309 . . . . . . . 8 (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9998rspcev 3581 . . . . . . 7 (((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
10013, 97, 99syl2anc 584 . . . . . 6 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
101 ustexhalf 23562 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
102101adantlr 713 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
103100, 102r19.29a 3159 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
104103adantr 481 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
105 eleq1 2825 . . . . . 6 (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
106105rexralbidv 3214 . . . . 5 (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
107106adantl 482 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
108104, 107mpbird 256 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
109108adantllr 717 . 2 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
110 vex 3449 . . . 4 𝑎 ∈ V
1119ustuqtoplem 23591 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
112110, 111mpan2 689 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
113112biimpa 477 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
114109, 113r19.29a 3159 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 3064  wrex 3073  Vcvv 3445  wss 3910  {csn 4586   class class class wbr 5105  cmpt 5188  ran crn 5634  cima 5636  ccom 5637  Rel wrel 5638  cfv 6496  UnifOncust 23551
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-rep 5242  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-reu 3354  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-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ust 23552
This theorem is referenced by:  ustuqtop  23598  utopsnneiplem  23599
  Copyright terms: Public domain W3C validator