Metamath Proof Explorer


Theorem ustuqtop4

Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
Assertion ustuqtop4 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 𝑁 = ( 𝑝𝑋 ↦ ran ( 𝑣𝑈 ↦ ( 𝑣 “ { 𝑝 } ) ) )
2 simplll ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) )
3 simplr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → 𝑢𝑈 )
4 eqid ( 𝑢 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } )
5 imaeq1 ( 𝑤 = 𝑢 → ( 𝑤 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) )
6 5 rspceeqv ( ( 𝑢𝑈 ∧ ( 𝑢 “ { 𝑝 } ) = ( 𝑢 “ { 𝑝 } ) ) → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) )
7 4 6 mpan2 ( 𝑢𝑈 → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) )
8 7 adantl ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑢𝑈 ) → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) )
9 imaexg ( 𝑢𝑈 → ( 𝑢 “ { 𝑝 } ) ∈ V )
10 1 ustuqtoplem ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ ( 𝑢 “ { 𝑝 } ) ∈ V ) → ( ( 𝑢 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑤𝑈 ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) ) )
11 9 10 sylan2 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑢𝑈 ) → ( ( 𝑢 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑤𝑈 ( 𝑢 “ { 𝑝 } ) = ( 𝑤 “ { 𝑝 } ) ) )
12 8 11 mpbird ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑢𝑈 ) → ( 𝑢 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) )
13 2 3 12 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → ( 𝑢 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) )
14 simp-5l ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
15 2 simpld ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
16 simp-4r ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → 𝑝𝑋 )
17 ustimasn ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢𝑈𝑝𝑋 ) → ( 𝑢 “ { 𝑝 } ) ⊆ 𝑋 )
18 15 3 16 17 syl3anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → ( 𝑢 “ { 𝑝 } ) ⊆ 𝑋 )
19 18 sselda ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → 𝑞𝑋 )
20 14 19 jca ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) )
21 simplr ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) )
22 simp-6l ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
23 simp-4r ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑢𝑈 )
24 ustrel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢𝑈 ) → Rel 𝑢 )
25 22 23 24 syl2anc ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → Rel 𝑢 )
26 elrelimasn ( Rel 𝑢 → ( 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ↔ 𝑝 𝑢 𝑞 ) )
27 25 26 syl ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → ( 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ↔ 𝑝 𝑢 𝑞 ) )
28 21 27 mpbid ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑝 𝑢 𝑞 )
29 simpr ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) )
30 elrelimasn ( Rel 𝑢 → ( 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ↔ 𝑞 𝑢 𝑟 ) )
31 25 30 syl ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → ( 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ↔ 𝑞 𝑢 𝑟 ) )
32 29 31 mpbid ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑞 𝑢 𝑟 )
33 vex 𝑝 ∈ V
34 vex 𝑟 ∈ V
35 33 34 brco ( 𝑝 ( 𝑢𝑢 ) 𝑟 ↔ ∃ 𝑞 ( 𝑝 𝑢 𝑞𝑞 𝑢 𝑟 ) )
36 35 biimpri ( ∃ 𝑞 ( 𝑝 𝑢 𝑞𝑞 𝑢 𝑟 ) → 𝑝 ( 𝑢𝑢 ) 𝑟 )
37 36 19.23bi ( ( 𝑝 𝑢 𝑞𝑞 𝑢 𝑟 ) → 𝑝 ( 𝑢𝑢 ) 𝑟 )
38 28 32 37 syl2anc ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑝 ( 𝑢𝑢 ) 𝑟 )
39 simpllr ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → ( 𝑢𝑢 ) ⊆ 𝑤 )
40 39 ssbrd ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → ( 𝑝 ( 𝑢𝑢 ) 𝑟𝑝 𝑤 𝑟 ) )
41 38 40 mpd ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑝 𝑤 𝑟 )
42 simp-5r ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑤𝑈 )
43 ustrel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈 ) → Rel 𝑤 )
44 22 42 43 syl2anc ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → Rel 𝑤 )
45 elrelimasn ( Rel 𝑤 → ( 𝑟 ∈ ( 𝑤 “ { 𝑝 } ) ↔ 𝑝 𝑤 𝑟 ) )
46 44 45 syl ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → ( 𝑟 ∈ ( 𝑤 “ { 𝑝 } ) ↔ 𝑝 𝑤 𝑟 ) )
47 41 46 mpbird ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) ∧ 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) ) → 𝑟 ∈ ( 𝑤 “ { 𝑝 } ) )
48 47 ex ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑟 ∈ ( 𝑢 “ { 𝑞 } ) → 𝑟 ∈ ( 𝑤 “ { 𝑝 } ) ) )
49 48 ssrdv ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) )
50 simp-4r ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → 𝑤𝑈 )
51 16 adantr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → 𝑝𝑋 )
52 ustimasn ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈𝑝𝑋 ) → ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 )
53 14 50 51 52 syl3anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 )
54 20 49 53 3jca ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) )
55 simpllr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → 𝑢𝑈 )
56 eqidd ( 𝑢𝑈 → ( 𝑢 “ { 𝑞 } ) = ( 𝑢 “ { 𝑞 } ) )
57 imaeq1 ( 𝑤 = 𝑢 → ( 𝑤 “ { 𝑞 } ) = ( 𝑢 “ { 𝑞 } ) )
58 57 rspceeqv ( ( 𝑢𝑈 ∧ ( 𝑢 “ { 𝑞 } ) = ( 𝑢 “ { 𝑞 } ) ) → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑞 } ) = ( 𝑤 “ { 𝑞 } ) )
59 56 58 mpdan ( 𝑢𝑈 → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑞 } ) = ( 𝑤 “ { 𝑞 } ) )
60 59 adantl ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑢𝑈 ) → ∃ 𝑤𝑈 ( 𝑢 “ { 𝑞 } ) = ( 𝑤 “ { 𝑞 } ) )
61 imaexg ( 𝑢𝑈 → ( 𝑢 “ { 𝑞 } ) ∈ V )
62 1 ustuqtoplem ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ V ) → ( ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ↔ ∃ 𝑤𝑈 ( 𝑢 “ { 𝑞 } ) = ( 𝑤 “ { 𝑞 } ) ) )
63 61 62 sylan2 ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑢𝑈 ) → ( ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ↔ ∃ 𝑤𝑈 ( 𝑢 “ { 𝑞 } ) = ( 𝑤 “ { 𝑞 } ) ) )
64 60 63 mpbird ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑢𝑈 ) → ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) )
65 14 19 55 64 syl21anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) )
66 54 65 jca ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) )
67 imaexg ( 𝑤𝑈 → ( 𝑤 “ { 𝑝 } ) ∈ V )
68 sseq2 ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏 ↔ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ) )
69 sseq1 ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( 𝑏𝑋 ↔ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) )
70 68 69 3anbi23d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ↔ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ) )
71 70 anbi1d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ↔ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ) )
72 71 anbi1d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) ↔ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) ) )
73 eleq1 ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( 𝑏 ∈ ( 𝑁𝑞 ) ↔ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
74 72 73 imbi12d ( 𝑏 = ( 𝑤 “ { 𝑝 } ) → ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) → 𝑏 ∈ ( 𝑁𝑞 ) ) ↔ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) ) )
75 sseq1 ( 𝑎 = ( 𝑢 “ { 𝑞 } ) → ( 𝑎𝑏 ↔ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏 ) )
76 75 3anbi2d ( 𝑎 = ( 𝑢 “ { 𝑞 } ) → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ↔ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ) )
77 eleq1 ( 𝑎 = ( 𝑢 “ { 𝑞 } ) → ( 𝑎 ∈ ( 𝑁𝑞 ) ↔ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) )
78 76 77 anbi12d ( 𝑎 = ( 𝑢 “ { 𝑞 } ) → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑞 ) ) ↔ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ) )
79 78 imbi1d ( 𝑎 = ( 𝑢 “ { 𝑞 } ) → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) ) ↔ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) ) ) )
80 eleq1 ( 𝑝 = 𝑞 → ( 𝑝𝑋𝑞𝑋 ) )
81 80 anbi2d ( 𝑝 = 𝑞 → ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ) )
82 81 3anbi1d ( 𝑝 = 𝑞 → ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ↔ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ) )
83 fveq2 ( 𝑝 = 𝑞 → ( 𝑁𝑝 ) = ( 𝑁𝑞 ) )
84 83 eleq2d ( 𝑝 = 𝑞 → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ 𝑎 ∈ ( 𝑁𝑞 ) ) )
85 82 84 anbi12d ( 𝑝 = 𝑞 → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) ↔ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑞 ) ) ) )
86 83 eleq2d ( 𝑝 = 𝑞 → ( 𝑏 ∈ ( 𝑁𝑝 ) ↔ 𝑏 ∈ ( 𝑁𝑞 ) ) )
87 85 86 imbi12d ( 𝑝 = 𝑞 → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑏 ∈ ( 𝑁𝑝 ) ) ↔ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) ) ) )
88 1 ustuqtop1 ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → 𝑏 ∈ ( 𝑁𝑝 ) )
89 87 88 chvarvv ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ 𝑎𝑏𝑏𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) )
90 79 89 vtoclg ( ( 𝑢 “ { 𝑞 } ) ∈ V → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) ) )
91 61 90 syl ( 𝑢𝑈 → ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) → 𝑏 ∈ ( 𝑁𝑞 ) ) )
92 91 impcom ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ 𝑏𝑏𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) → 𝑏 ∈ ( 𝑁𝑞 ) )
93 74 92 vtoclg ( ( 𝑤 “ { 𝑝 } ) ∈ V → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
94 67 93 syl ( 𝑤𝑈 → ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
95 94 impcom ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑞𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ⊆ ( 𝑤 “ { 𝑝 } ) ∧ ( 𝑤 “ { 𝑝 } ) ⊆ 𝑋 ) ∧ ( 𝑢 “ { 𝑞 } ) ∈ ( 𝑁𝑞 ) ) ∧ 𝑢𝑈 ) ∧ 𝑤𝑈 ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
96 66 55 50 95 syl21anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) ∧ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ) → ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
97 96 ralrimiva ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → ∀ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
98 raleq ( 𝑏 = ( 𝑢 “ { 𝑝 } ) → ( ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ↔ ∀ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
99 98 rspcev ( ( ( 𝑢 “ { 𝑝 } ) ∈ ( 𝑁𝑝 ) ∧ ∀ 𝑞 ∈ ( 𝑢 “ { 𝑝 } ) ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
100 13 97 99 syl2anc ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑢𝑈 ) ∧ ( 𝑢𝑢 ) ⊆ 𝑤 ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
101 ustexhalf ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈 ) → ∃ 𝑢𝑈 ( 𝑢𝑢 ) ⊆ 𝑤 )
102 101 adantlr ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) → ∃ 𝑢𝑈 ( 𝑢𝑢 ) ⊆ 𝑤 )
103 100 102 r19.29a ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
104 103 adantr ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) )
105 eleq1 ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → ( 𝑎 ∈ ( 𝑁𝑞 ) ↔ ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
106 105 rexralbidv ( 𝑎 = ( 𝑤 “ { 𝑝 } ) → ( ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) ↔ ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
107 106 adantl ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ( ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) ↔ ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 ( 𝑤 “ { 𝑝 } ) ∈ ( 𝑁𝑞 ) ) )
108 104 107 mpbird ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑤𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) )
109 108 adantllr ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) ∧ 𝑤𝑈 ) ∧ 𝑎 = ( 𝑤 “ { 𝑝 } ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) )
110 vex 𝑎 ∈ V
111 1 ustuqtoplem ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ V ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑤𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
112 110 111 mpan2 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) → ( 𝑎 ∈ ( 𝑁𝑝 ) ↔ ∃ 𝑤𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) ) )
113 112 biimpa ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → ∃ 𝑤𝑈 𝑎 = ( 𝑤 “ { 𝑝 } ) )
114 109 113 r19.29a ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑝𝑋 ) ∧ 𝑎 ∈ ( 𝑁𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁𝑝 ) ∀ 𝑞𝑏 𝑎 ∈ ( 𝑁𝑞 ) )