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

Theorem ustuqtop4 22095
Description: Lemma for ustuqtop 22097. (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 813 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋))
2 simplr 807 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑢𝑈)
3 eqid 2651 . . . . . . . . . . 11 (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})
4 imaeq1 5496 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))
54eqeq2d 2661 . . . . . . . . . . . 12 (𝑤 = 𝑢 → ((𝑢 “ {𝑝}) = (𝑤 “ {𝑝}) ↔ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})))
65rspcev 3340 . . . . . . . . . . 11 ((𝑢𝑈 ∧ (𝑢 “ {𝑝}) = (𝑢 “ {𝑝})) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
73, 6mpan2 707 . . . . . . . . . 10 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
87adantl 481 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝}))
9 imaexg 7145 . . . . . . . . . 10 (𝑢𝑈 → (𝑢 “ {𝑝}) ∈ V)
10 utopustuq.1 . . . . . . . . . . 11 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
1110ustuqtoplem 22090 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ (𝑢 “ {𝑝}) ∈ V) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
129, 11sylan2 490 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})))
138, 12mpbird 247 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
141, 2, 13syl2anc 694 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ∈ (𝑁𝑝))
15 simp-5l 825 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
161simpld 474 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑈 ∈ (UnifOn‘𝑋))
17 simp-4r 824 . . . . . . . . . . . . . 14 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → 𝑝𝑋)
18 ustimasn 22079 . . . . . . . . . . . . . 14 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑝𝑋) → (𝑢 “ {𝑝}) ⊆ 𝑋)
1916, 2, 17, 18syl3anc 1366 . . . . . . . . . . . . 13 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → (𝑢 “ {𝑝}) ⊆ 𝑋)
2019sselda 3636 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑞𝑋)
2115, 20jca 553 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋))
22 simplr 807 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞 ∈ (𝑢 “ {𝑝}))
23 simp-6l 827 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑈 ∈ (UnifOn‘𝑋))
24 simp-4r 824 . . . . . . . . . . . . . . . . . . 19 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑢𝑈)
25 ustrel 22062 . . . . . . . . . . . . . . . . . . 19 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → Rel 𝑢)
2623, 24, 25syl2anc 694 . . . . . . . . . . . . . . . . . 18 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑢)
27 elrelimasn 5524 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2826, 27syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑞 ∈ (𝑢 “ {𝑝}) ↔ 𝑝𝑢𝑞))
2922, 28mpbid 222 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑢𝑞)
30 simpr 476 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑢 “ {𝑞}))
31 elrelimasn 5524 . . . . . . . . . . . . . . . . . 18 (Rel 𝑢 → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3226, 31syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑢 “ {𝑞}) ↔ 𝑞𝑢𝑟))
3330, 32mpbid 222 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑞𝑢𝑟)
34 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑝 ∈ V
35 vex 3234 . . . . . . . . . . . . . . . . . . 19 𝑟 ∈ V
3634, 35brco 5325 . . . . . . . . . . . . . . . . . 18 (𝑝(𝑢𝑢)𝑟 ↔ ∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟))
3736biimpri 218 . . . . . . . . . . . . . . . . 17 (∃𝑞(𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
383719.23bi 2099 . . . . . . . . . . . . . . . 16 ((𝑝𝑢𝑞𝑞𝑢𝑟) → 𝑝(𝑢𝑢)𝑟)
3929, 33, 38syl2anc 694 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝(𝑢𝑢)𝑟)
40 simpllr 815 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑢𝑢) ⊆ 𝑤)
4140ssbrd 4728 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑝(𝑢𝑢)𝑟𝑝𝑤𝑟))
4239, 41mpd 15 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑝𝑤𝑟)
43 simp-5r 826 . . . . . . . . . . . . . . . 16 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑤𝑈)
44 ustrel 22062 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → Rel 𝑤)
4523, 43, 44syl2anc 694 . . . . . . . . . . . . . . 15 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → Rel 𝑤)
46 elrelimasn 5524 . . . . . . . . . . . . . . 15 (Rel 𝑤 → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4745, 46syl 17 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → (𝑟 ∈ (𝑤 “ {𝑝}) ↔ 𝑝𝑤𝑟))
4842, 47mpbird 247 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) ∧ 𝑟 ∈ (𝑢 “ {𝑞})) → 𝑟 ∈ (𝑤 “ {𝑝}))
4948ex 449 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑟 ∈ (𝑢 “ {𝑞}) → 𝑟 ∈ (𝑤 “ {𝑝})))
5049ssrdv 3642 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}))
51 simp-4r 824 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑤𝑈)
5217adantr 480 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑝𝑋)
53 ustimasn 22079 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈𝑝𝑋) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5415, 51, 52, 53syl3anc 1366 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ⊆ 𝑋)
5521, 50, 543jca 1261 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋))
56 simpllr 815 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → 𝑢𝑈)
57 eqidd 2652 . . . . . . . . . . . . . 14 (𝑢𝑈 → (𝑢 “ {𝑞}) = (𝑢 “ {𝑞}))
58 imaeq1 5496 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑢 → (𝑤 “ {𝑞}) = (𝑢 “ {𝑞}))
5958eqeq2d 2661 . . . . . . . . . . . . . . 15 (𝑤 = 𝑢 → ((𝑢 “ {𝑞}) = (𝑤 “ {𝑞}) ↔ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})))
6059rspcev 3340 . . . . . . . . . . . . . 14 ((𝑢𝑈 ∧ (𝑢 “ {𝑞}) = (𝑢 “ {𝑞})) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6157, 60mpdan 703 . . . . . . . . . . . . 13 (𝑢𝑈 → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
6261adantl 481 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞}))
63 imaexg 7145 . . . . . . . . . . . . 13 (𝑢𝑈 → (𝑢 “ {𝑞}) ∈ V)
6410ustuqtoplem 22090 . . . . . . . . . . . . 13 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ∈ V) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6563, 64sylan2 490 . . . . . . . . . . . 12 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → ((𝑢 “ {𝑞}) ∈ (𝑁𝑞) ↔ ∃𝑤𝑈 (𝑢 “ {𝑞}) = (𝑤 “ {𝑞})))
6662, 65mpbird 247 . . . . . . . . . . 11 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑢𝑈) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6715, 20, 56, 66syl21anc 1365 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑢 “ {𝑞}) ∈ (𝑁𝑞))
6855, 67jca 553 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
69 imaexg 7145 . . . . . . . . . . 11 (𝑤𝑈 → (𝑤 “ {𝑝}) ∈ V)
70 sseq2 3660 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → ((𝑢 “ {𝑞}) ⊆ 𝑏 ↔ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝})))
71 sseq1 3659 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑤 “ {𝑝}) → (𝑏𝑋 ↔ (𝑤 “ {𝑝}) ⊆ 𝑋))
7270, 713anbi23d 1442 . . . . . . . . . . . . . . 15 (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋)))
7372anbi1d 741 . . . . . . . . . . . . . 14 (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
7473anbi1d 741 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈)))
75 eleq1 2718 . . . . . . . . . . . . 13 (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
7674, 75imbi12d 333 . . . . . . . . . . . 12 (𝑏 = (𝑤 “ {𝑝}) → ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞)) ↔ (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))))
77 sseq1 3659 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑢 “ {𝑞}) → (𝑎𝑏 ↔ (𝑢 “ {𝑞}) ⊆ 𝑏))
78773anbi2d 1444 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋)))
79 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑢 “ {𝑞}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)))
8078, 79anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑢 “ {𝑞}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞))))
8180imbi1d 330 . . . . . . . . . . . . . . 15 (𝑎 = (𝑢 “ {𝑞}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
82 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝𝑋𝑞𝑋))
8382anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋)))
84833anbi1d 1443 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋)))
85 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → (𝑁𝑝) = (𝑁𝑞))
8685eleq2d 2716 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑎 ∈ (𝑁𝑝) ↔ 𝑎 ∈ (𝑁𝑞)))
8784, 86anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞))))
8885eleq2d 2716 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (𝑏 ∈ (𝑁𝑝) ↔ 𝑏 ∈ (𝑁𝑞)))
8987, 88imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))))
9010ustuqtop1 22092 . . . . . . . . . . . . . . . 16 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
9189, 90chvarv 2299 . . . . . . . . . . . . . . 15 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞))
9281, 91vtoclg 3297 . . . . . . . . . . . . . 14 ((𝑢 “ {𝑞}) ∈ V → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9363, 92syl 17 . . . . . . . . . . . . 13 (𝑢𝑈 → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) → 𝑏 ∈ (𝑁𝑞)))
9493impcom 445 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ 𝑏𝑏𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → 𝑏 ∈ (𝑁𝑞))
9576, 94vtoclg 3297 . . . . . . . . . . 11 ((𝑤 “ {𝑝}) ∈ V → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9669, 95syl 17 . . . . . . . . . 10 (𝑤𝑈 → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
9796impcom 445 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑞𝑋) ∧ (𝑢 “ {𝑞}) ⊆ (𝑤 “ {𝑝}) ∧ (𝑤 “ {𝑝}) ⊆ 𝑋) ∧ (𝑢 “ {𝑞}) ∈ (𝑁𝑞)) ∧ 𝑢𝑈) ∧ 𝑤𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9868, 56, 51, 97syl21anc 1365 . . . . . . . 8 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) ∧ 𝑞 ∈ (𝑢 “ {𝑝})) → (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
9998ralrimiva 2995 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞))
100 raleq 3168 . . . . . . . 8 (𝑏 = (𝑢 “ {𝑝}) → (∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞) ↔ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
101100rspcev 3340 . . . . . . 7 (((𝑢 “ {𝑝}) ∈ (𝑁𝑝) ∧ ∀𝑞 ∈ (𝑢 “ {𝑝})(𝑤 “ {𝑝}) ∈ (𝑁𝑞)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
10214, 99, 101syl2anc 694 . . . . . 6 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑤) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
103 ustexhalf 22061 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
104103adantlr 751 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑤)
105102, 104r19.29a 3107 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
106105adantr 480 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞))
107 eleq1 2718 . . . . . 6 (𝑎 = (𝑤 “ {𝑝}) → (𝑎 ∈ (𝑁𝑞) ↔ (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
108107rexralbidv 3087 . . . . 5 (𝑎 = (𝑤 “ {𝑝}) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
109108adantl 481 . . . 4 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞) ↔ ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 (𝑤 “ {𝑝}) ∈ (𝑁𝑞)))
110106, 109mpbird 247 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
111110adantllr 755 . 2 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
112 vex 3234 . . . 4 𝑎 ∈ V
11310ustuqtoplem 22090 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
114112, 113mpan2 707 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
115114biimpa 500 . 2 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
116111, 115r19.29a 3107 1 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑏 ∈ (𝑁𝑝)∀𝑞𝑏 𝑎 ∈ (𝑁𝑞))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  Vcvv 3231  wss 3607  {csn 4210   class class class wbr 4685  cmpt 4762  ran crn 5144  cima 5146  ccom 5147  Rel wrel 5148  cfv 5926  UnifOncust 22050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ust 22051
This theorem is referenced by:  ustuqtop  22097  utopsnneiplem  22098
  Copyright terms: Public domain W3C validator