MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trust Structured version   Visualization version   GIF version
Theorem trust 24054
Description: The trace of a uniform structure π‘ˆ on a subset 𝐴 is a uniform structure on 𝐴. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)
Assertion
Ref Expression
trust ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∈ (UnifOnβ€˜π΄))
Proof of Theorem trust
Dummy variables 𝑣 𝑒 𝑀 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 restsspw 17384 . . . 4 (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴)
21a1i 11 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴))
3 inxp 5832 . . . . . 6 ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = ((𝑋 ∩ 𝐴) Γ— (𝑋 ∩ 𝐴))
4 sseqin2 4215 . . . . . . . 8 (𝐴 βŠ† 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
54biimpi 215 . . . . . . 7 (𝐴 βŠ† 𝑋 β†’ (𝑋 ∩ 𝐴) = 𝐴)
65sqxpeqd 5708 . . . . . 6 (𝐴 βŠ† 𝑋 β†’ ((𝑋 ∩ 𝐴) Γ— (𝑋 ∩ 𝐴)) = (𝐴 Γ— 𝐴))
73, 6eqtrid 2783 . . . . 5 (𝐴 βŠ† 𝑋 β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = (𝐴 Γ— 𝐴))
87adantl 481 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = (𝐴 Γ— 𝐴))
9 simpl 482 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
10 elfvex 6929 . . . . . . . 8 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 ∈ V)
1110adantr 480 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 ∈ V)
12 simpr 484 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 βŠ† 𝑋)
1311, 12ssexd 5324 . . . . . 6 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ V)
1413, 13xpexd 7742 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ V)
15 ustbasel 24031 . . . . . 6 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) ∈ π‘ˆ)
1615adantr 480 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑋 Γ— 𝑋) ∈ π‘ˆ)
17 elrestr 17381 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V ∧ (𝑋 Γ— 𝑋) ∈ π‘ˆ) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
189, 14, 16, 17syl3anc 1370 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
198, 18eqeltrrd 2833 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
209ad5antr 731 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
2114ad5antr 731 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
22 simplr 766 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ π‘ˆ)
23 simp-4r 781 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴))
2423elpwid 4611 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 βŠ† (𝐴 Γ— 𝐴))
2512ad5antr 731 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝐴 βŠ† 𝑋)
26 xpss12 5691 . . . . . . . . . . . . . 14 ((𝐴 βŠ† 𝑋 ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
2725, 25, 26syl2anc 583 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
2824, 27sstrd 3992 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
29 ustssxp 24029 . . . . . . . . . . . . 13 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
3020, 22, 29syl2anc 583 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
3128, 30unssd 4186 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋))
32 ssun2 4173 . . . . . . . . . . . 12 𝑒 βŠ† (𝑀 βˆͺ 𝑒)
33 ustssel 24030 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑒 βŠ† (𝑀 βˆͺ 𝑒) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ))
3432, 33mpi 20 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ)
3520, 22, 31, 34syl3anc 1370 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ)
36 df-ss 3965 . . . . . . . . . . . . . 14 (𝑀 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) = 𝑀)
3724, 36sylib 217 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = 𝑀)
3837uneq1d 4162 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))))
39 simpr 484 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
40 simpllr 773 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 βŠ† 𝑀)
4139, 40eqsstrrd 4021 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑒 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑀)
42 ssequn2 4183 . . . . . . . . . . . . 13 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑀 ↔ (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = 𝑀)
4341, 42sylib 217 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = 𝑀)
4438, 43eqtr2d 2772 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 = ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))))
45 indir 4275 . . . . . . . . . . 11 ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)) = ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴)))
4644, 45eqtr4di 2789 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)))
47 ineq1 4205 . . . . . . . . . . 11 (π‘₯ = (𝑀 βˆͺ 𝑒) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)))
4847rspceeqv 3633 . . . . . . . . . 10 (((𝑀 βˆͺ 𝑒) ∈ π‘ˆ ∧ 𝑀 = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
4935, 46, 48syl2anc 583 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
50 elrest 17380 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
5150biimpar 477 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
5220, 21, 49, 51syl21anc 835 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
53 elrest 17380 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))))
5453biimpa 476 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5514, 54syldanl 601 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5655ad2antrr 723 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5752, 56r19.29a 3161 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
5857ex 412 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) β†’ (𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))))
5958ralrimiva 3145 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))))
609ad5antr 731 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
6114ad5antr 731 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝐴 Γ— 𝐴) ∈ V)
62 simpllr 773 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑒 ∈ π‘ˆ)
63 simplr 766 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ π‘₯ ∈ π‘ˆ)
64 ustincl 24032 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ π‘₯ ∈ π‘ˆ) β†’ (𝑒 ∩ π‘₯) ∈ π‘ˆ)
6560, 62, 63, 64syl3anc 1370 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑒 ∩ π‘₯) ∈ π‘ˆ)
66 simprl 768 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
67 simprr 770 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
6866, 67ineq12d 4213 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) ∩ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
69 inindir 4227 . . . . . . . . . 10 ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) ∩ (π‘₯ ∩ (𝐴 Γ— 𝐴)))
7068, 69eqtr4di 2789 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)))
71 ineq1 4205 . . . . . . . . . 10 (𝑦 = (𝑒 ∩ π‘₯) β†’ (𝑦 ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)))
7271rspceeqv 3633 . . . . . . . . 9 (((𝑒 ∩ π‘₯) ∈ π‘ˆ ∧ (𝑣 ∩ 𝑀) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴)))
7365, 70, 72syl2anc 583 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴)))
74 elrest 17380 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ ((𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴))))
7574biimpar 477 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
7660, 61, 73, 75syl21anc 835 . . . . . . 7 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
7755adantr 480 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
789ad2antrr 723 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
7914ad2antrr 723 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
80 simpr 484 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
8150biimpa 476 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
8278, 79, 80, 81syl21anc 835 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
83 reeanv 3225 . . . . . . . 8 (βˆƒπ‘’ ∈ π‘ˆ βˆƒπ‘₯ ∈ π‘ˆ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) ↔ (βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
8477, 82, 83sylanbrc 582 . . . . . . 7 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ βˆƒπ‘₯ ∈ π‘ˆ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
8576, 84r19.29vva 3212 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
8685ralrimiva 3145 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
87 simp-4l 780 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
88 simplr 766 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ π‘ˆ)
89 ustdiag 24033 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ ( I β†Ύ 𝑋) βŠ† 𝑒)
9087, 88, 89syl2anc 583 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝑋) βŠ† 𝑒)
91 simp-4r 781 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝐴 βŠ† 𝑋)
92 inss1 4228 . . . . . . . . . . . . . 14 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† ( I β†Ύ 𝑋)
93 resss 6006 . . . . . . . . . . . . . 14 ( I β†Ύ 𝑋) βŠ† I
9492, 93sstri 3991 . . . . . . . . . . . . 13 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† I
95 iss 6035 . . . . . . . . . . . . 13 ((( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† I ↔ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴))))
9694, 95mpbi 229 . . . . . . . . . . . 12 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
97 simpr 484 . . . . . . . . . . . . . . . 16 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝐴)
98 ssel2 3977 . . . . . . . . . . . . . . . . 17 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝑋)
99 equid 2014 . . . . . . . . . . . . . . . . . 18 𝑒 = 𝑒
100 resieq 5992 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ 𝑋 ∧ 𝑒 ∈ 𝑋) β†’ (𝑒( I β†Ύ 𝑋)𝑒 ↔ 𝑒 = 𝑒))
10199, 100mpbiri 258 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ 𝑋 ∧ 𝑒 ∈ 𝑋) β†’ 𝑒( I β†Ύ 𝑋)𝑒)
10298, 98, 101syl2anc 583 . . . . . . . . . . . . . . . 16 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒( I β†Ύ 𝑋)𝑒)
103 breq2 5152 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑒 β†’ (𝑒( I β†Ύ 𝑋)𝑣 ↔ 𝑒( I β†Ύ 𝑋)𝑒))
104103rspcev 3612 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ 𝐴 ∧ 𝑒( I β†Ύ 𝑋)𝑒) β†’ βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
10597, 102, 104syl2anc 583 . . . . . . . . . . . . . . 15 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
106105ralrimiva 3145 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝑋 β†’ βˆ€π‘’ ∈ 𝐴 βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
107 dminxp 6179 . . . . . . . . . . . . . 14 (dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = 𝐴 ↔ βˆ€π‘’ ∈ 𝐴 βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
108106, 107sylibr 233 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝑋 β†’ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = 𝐴)
109108reseq2d 5981 . . . . . . . . . . . 12 (𝐴 βŠ† 𝑋 β†’ ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴))) = ( I β†Ύ 𝐴))
11096, 109eqtr2id 2784 . . . . . . . . . . 11 (𝐴 βŠ† 𝑋 β†’ ( I β†Ύ 𝐴) = (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
111110adantl 481 . . . . . . . . . 10 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ ( I β†Ύ 𝐴) = (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
112 ssrin 4233 . . . . . . . . . . 11 (( I β†Ύ 𝑋) βŠ† 𝑒 β†’ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
113112adantr 480 . . . . . . . . . 10 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
114111, 113eqsstrd 4020 . . . . . . . . 9 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ ( I β†Ύ 𝐴) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
11590, 91, 114syl2anc 583 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
116 simpr 484 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
117115, 116sseqtrrd 4023 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† 𝑣)
118117, 55r19.29a 3161 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† 𝑣)
11914ad3antrrr 727 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
120 ustinvel 24034 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ ◑𝑒 ∈ π‘ˆ)
12187, 88, 120syl2anc 583 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑒 ∈ π‘ˆ)
122116cnveqd 5875 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 = β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)))
123 cnvin 6144 . . . . . . . . . . 11 β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ β—‘(𝐴 Γ— 𝐴))
124 cnvxp 6156 . . . . . . . . . . . 12 β—‘(𝐴 Γ— 𝐴) = (𝐴 Γ— 𝐴)
125124ineq2i 4209 . . . . . . . . . . 11 (◑𝑒 ∩ β—‘(𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴))
126123, 125eqtri 2759 . . . . . . . . . 10 β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴))
127122, 126eqtrdi 2787 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 = (◑𝑒 ∩ (𝐴 Γ— 𝐴)))
128 ineq1 4205 . . . . . . . . . 10 (π‘₯ = ◑𝑒 β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴)))
129128rspceeqv 3633 . . . . . . . . 9 ((◑𝑒 ∈ π‘ˆ ∧ ◑𝑣 = (◑𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
130121, 127, 129syl2anc 583 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
131 elrest 17380 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
132131biimpar 477 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
13387, 119, 130, 132syl21anc 835 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
134133, 55r19.29a 3161 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
135 simp-4l 780 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
13614ad3antrrr 727 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ (𝐴 Γ— 𝐴) ∈ V)
137 simplr 766 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ π‘₯ ∈ π‘ˆ)
138 elrestr 17381 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V ∧ π‘₯ ∈ π‘ˆ) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
139135, 136, 137, 138syl3anc 1370 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
140 inss1 4228 . . . . . . . . . . . . . . 15 (π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯
141 coss1 5855 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
142 coss2 5856 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ (π‘₯ ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯))
143141, 142sstrd 3992 . . . . . . . . . . . . . . 15 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯))
144140, 143ax-mp 5 . . . . . . . . . . . . . 14 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯)
145 sstr 3990 . . . . . . . . . . . . . 14 ((((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
146144, 145mpan 687 . . . . . . . . . . . . 13 ((π‘₯ ∘ π‘₯) βŠ† 𝑒 β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
147146adantl 481 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
148 inss2 4229 . . . . . . . . . . . . . . 15 (π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
149 coss1 5855 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
150 coss2 5856 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((𝐴 Γ— 𝐴) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)))
151149, 150sstrd 3992 . . . . . . . . . . . . . . 15 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)))
152148, 151ax-mp 5 . . . . . . . . . . . . . 14 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴))
153 xpidtr 6123 . . . . . . . . . . . . . 14 ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
154152, 153sstri 3991 . . . . . . . . . . . . 13 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝐴 Γ— 𝐴)
155154a1i 11 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝐴 Γ— 𝐴))
156147, 155ssind 4232 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
157 id 22 . . . . . . . . . . . . . 14 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
158157, 157coeq12d 5864 . . . . . . . . . . . . 13 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ (𝑀 ∘ 𝑀) = ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
159158sseq1d 4013 . . . . . . . . . . . 12 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)) ↔ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
160159rspcev 3612 . . . . . . . . . . 11 (((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
161139, 156, 160syl2anc 583 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
162 ustexhalf 24035 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘₯ ∈ π‘ˆ (π‘₯ ∘ π‘₯) βŠ† 𝑒)
163162adantlr 712 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘₯ ∈ π‘ˆ (π‘₯ ∘ π‘₯) βŠ† 𝑒)
164161, 163r19.29a 3161 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
165164ad4ant13 748 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
166116sseq2d 4014 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ((𝑀 ∘ 𝑀) βŠ† 𝑣 ↔ (𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
167166rexbidv 3177 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣 ↔ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
168165, 167mpbird 257 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)
169168, 55r19.29a 3161 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)
170118, 134, 1693jca 1127 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣))
17159, 86, 1703jca 1127 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))
172171ralrimiva 3145 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))
1732, 19, 1723jca 1127 . 2 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴) ∧ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣))))
174 isust 24028 . . 3 (𝐴 ∈ V β†’ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∈ (UnifOnβ€˜π΄) ↔ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴) ∧ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))))
17513, 174syl 17 . 2 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∈ (UnifOnβ€˜π΄) ↔ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴) ∧ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))))
176173, 175mpbird 257 1 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∈ (UnifOnβ€˜π΄))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602   class class class wbr 5148   I cid 5573   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676   β†Ύ cres 5678   ∘ ccom 5680  β€˜cfv 6543  (class class class)co 7412   β†Ύt crest 17373  UnifOncust 24024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-rest 17375  df-ust 24025
This theorem is referenced by:  restutop  24062  restutopopn  24063  ressust  24088  ressusp  24089  trcfilu  24119  cfiluweak  24120
  Copyright terms: Public domain W3C validator