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 ‘ 𝑋 ) ∧ 𝑝 ∈ 𝑋 ) ∧ 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ) → ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑝 ) ∀ 𝑞 ∈ 𝑏 𝑎 ∈ ( 𝑁 ‘ 𝑞 ) )