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

Theorem ustuqtop4 21971
 Description: Lemma for ustuqtop 21973. (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 797 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋))
2 simplr 791 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑢𝑈)
3 eqid 2621 . . . . . . . . . . 11 (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4 imaeq1 5425 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
54eqeq2d 2631 . . . . . . . . . . . 12 (𝑤 = 𝑢 → ((𝑢 “ {𝑝}) = (𝑤 “ {𝑝}) ↔ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})))
65rspcev 3298 . . . . . . . . . . 11 ((𝑢𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
73, 6mpan2 706 . . . . . . . . . 10 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
87adantl 482 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
9 imaexg 7057 . . . . . . . . . 10 (𝑢𝑈 → (𝑢 “ {𝑝}) ∈ V)
10 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
1110ustuqtoplem 21966 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
129, 11sylan2 491 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
138, 12mpbird 247 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
141, 2, 13syl2anc 692 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
15 simp-5l 807 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
161simpld 475 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
17 simp-4r 806 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑝𝑋)
18 ustimasn 21955 . . . . . . . . . . . . . 14 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑝𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1916, 2, 17, 18syl3anc 1323 . . . . . . . . . . . . 13 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
2019sselda 3587 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞𝑋)
2115, 20jca 554 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋))
22 simplr 791 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
23 simp-6l 809 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
24 simp-4r 806 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢𝑈)
25 ustrel 21938 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → Rel 𝑢)
2623, 24, 25syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
27 elrelimasn 5453 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2922, 28mpbid 222 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
30 simpr 477 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
31 elrelimasn 5453 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3226, 31syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3330, 32mpbid 222 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
34 vex 3192 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
35 vex 3192 . . . . . . . . . . . . . . . . . . 19 𝑟 ∈ V
3634, 35brco 5257 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑢𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟))
3736biimpri 218 . . . . . . . . . . . . . . . . 17 (∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
383719.23bi 2059 . . . . . . . . . . . . . . . 16 ((𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
3929, 33, 38syl2anc 692 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢𝑢)𝑟)
40 simpllr 798 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢𝑢) ⊆ 𝑤)
4140ssbrd 4661 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢𝑢)𝑟𝑝𝑤𝑟))
4239, 41mpd 15 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
43 simp-5r 808 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤𝑈)
44 ustrel 21938 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → Rel 𝑤)
4523, 43, 44syl2anc 692 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
46 elrelimasn 5453 . . . . . . . . . . . . . . 15 (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4745, 46syl 17 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4842, 47mpbird 247 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
4948ex 450 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
5049ssrdv 3593 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
51 simp-4r 806 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤𝑈)
5217adantr 481 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝𝑋)
53 ustimasn 21955 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈𝑝𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5415, 51, 52, 53syl3anc 1323 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5521, 50, 543jca 1240 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
56 simpllr 798 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢𝑈)
57 eqidd 2622 . . . . . . . . . . . . . 14 (𝑢𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
58 imaeq1 5425 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
5958eqeq2d 2631 . . . . . . . . . . . . . . 15 (𝑤 = 𝑢 → ((𝑢 “ {𝑞}) = (𝑤 “ {𝑞}) ↔ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})))
6059rspcev 3298 . . . . . . . . . . . . . 14 ((𝑢𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6157, 60mpdan 701 . . . . . . . . . . . . 13 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6261adantl 482 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
63 imaexg 7057 . . . . . . . . . . . . 13 (𝑢𝑈 → (𝑢 “ {𝑞}) ∈ V)
6410ustuqtoplem 21966 . . . . . . . . . . . . 13 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6563, 64sylan2 491 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6662, 65mpbird 247 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6715, 20, 56, 66syl21anc 1322 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6855, 67jca 554 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
69 imaexg 7057 . . . . . . . . . . 11 (𝑤𝑈 → (𝑤 “ {𝑝}) ∈ V)
70 sseq2 3611 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
71 sseq1 3610 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → (𝑏𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
7270, 713anbi23d 1399 . . . . . . . . . . . . . . 15 (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
7372anbi1d 740 . . . . . . . . . . . . . 14 (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7473anbi1d 740 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈)))
75 eleq1 2686 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
7674, 75imbi12d 334 . . . . . . . . . . . 12 (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))))
77 sseq1 3610 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑢 “ {𝑞}) → (𝑎𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
78773anbi2d 1401 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋)))
79 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
8078, 79anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
8180imbi1d 331 . . . . . . . . . . . . . . 15 (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
82 eleq1 2686 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
8382anbi2d 739 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋)))
84833anbi1d 1400 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋)))
85 fveq2 6153 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
8685eleq2d 2684 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑞)))
8784, 86anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞))))
8885eleq2d 2684 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑞)))
8987, 88imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
9010ustuqtop1 21968 . . . . . . . . . . . . . . . 16 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
9189, 90chvarv 2262 . . . . . . . . . . . . . . 15 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))
9281, 91vtoclg 3255 . . . . . . . . . . . . . 14 ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9363, 92syl 17 . . . . . . . . . . . . 13 (𝑢𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9493impcom 446 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞))
9576, 94vtoclg 3255 . . . . . . . . . . 11 ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9669, 95syl 17 . . . . . . . . . 10 (𝑤𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9796impcom 446 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ∧ 𝑤𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9868, 56, 51, 97syl21anc 1322 . . . . . . . 8 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9998ralrimiva 2961 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞))
100 raleq 3130 . . . . . . . 8 (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
101100rspcev 3298 . . . . . . 7 (((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
10214, 99, 101syl2anc 692 . . . . . 6 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
103 ustexhalf 21937 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
104103adantlr 750 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
105102, 104r19.29a 3072 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
106105adantr 481 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
107 eleq1 2686 . . . . . 6 (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
108107rexralbidv 3052 . . . . 5 (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
109108adantl 482 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
110106, 109mpbird 247 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
111110adantllr 754 . 2 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
112 vex 3192 . . . 4 𝑎 ∈ V
11310ustuqtoplem 21966 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
114112, 113mpan2 706 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
115114biimpa 501 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
116111, 115r19.29a 3072 1 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  Vcvv 3189   ⊆ wss 3559  {csn 4153   class class class wbr 4618   ↦ cmpt 4678  ran crn 5080   “ cima 5082   ∘ ccom 5083  Rel wrel 5084  ‘cfv 5852  UnifOncust 21926 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ust 21927 This theorem is referenced by:  ustuqtop  21973  utopsnneiplem  21974
 Copyright terms: Public domain W3C validator