MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trust Structured version   Visualization version   GIF version
Theorem trust 23716
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 17373 . . . 4 (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴)
21a1i 11 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴))
3 inxp 5830 . . . . . 6 ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = ((𝑋 ∩ 𝐴) Γ— (𝑋 ∩ 𝐴))
4 sseqin2 4214 . . . . . . . 8 (𝐴 βŠ† 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴)
54biimpi 215 . . . . . . 7 (𝐴 βŠ† 𝑋 β†’ (𝑋 ∩ 𝐴) = 𝐴)
65sqxpeqd 5707 . . . . . 6 (𝐴 βŠ† 𝑋 β†’ ((𝑋 ∩ 𝐴) Γ— (𝑋 ∩ 𝐴)) = (𝐴 Γ— 𝐴))
73, 6eqtrid 2785 . . . . 5 (𝐴 βŠ† 𝑋 β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = (𝐴 Γ— 𝐴))
87adantl 483 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) = (𝐴 Γ— 𝐴))
9 simpl 484 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
10 elfvex 6926 . . . . . . . 8 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 ∈ V)
1110adantr 482 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝑋 ∈ V)
12 simpr 486 . . . . . . 7 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 βŠ† 𝑋)
1311, 12ssexd 5323 . . . . . 6 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ 𝐴 ∈ V)
1413, 13xpexd 7733 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ V)
15 ustbasel 23693 . . . . . 6 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) ∈ π‘ˆ)
1615adantr 482 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝑋 Γ— 𝑋) ∈ π‘ˆ)
17 elrestr 17370 . . . . 5 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V ∧ (𝑋 Γ— 𝑋) ∈ π‘ˆ) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
189, 14, 16, 17syl3anc 1372 . . . 4 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((𝑋 Γ— 𝑋) ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
198, 18eqeltrrd 2835 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
209ad5antr 733 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
2114ad5antr 733 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
22 simplr 768 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ π‘ˆ)
23 simp-4r 783 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴))
2423elpwid 4610 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 βŠ† (𝐴 Γ— 𝐴))
2512ad5antr 733 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝐴 βŠ† 𝑋)
26 xpss12 5690 . . . . . . . . . . . . . 14 ((𝐴 βŠ† 𝑋 ∧ 𝐴 βŠ† 𝑋) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
2725, 25, 26syl2anc 585 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) βŠ† (𝑋 Γ— 𝑋))
2824, 27sstrd 3991 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
29 ustssxp 23691 . . . . . . . . . . . . 13 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
3020, 22, 29syl2anc 585 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 βŠ† (𝑋 Γ— 𝑋))
3128, 30unssd 4185 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋))
32 ssun2 4172 . . . . . . . . . . . 12 𝑒 βŠ† (𝑀 βˆͺ 𝑒)
33 ustssel 23692 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑒 βŠ† (𝑀 βˆͺ 𝑒) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ))
3432, 33mpi 20 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ (𝑀 βˆͺ 𝑒) βŠ† (𝑋 Γ— 𝑋)) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ)
3520, 22, 31, 34syl3anc 1372 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ 𝑒) ∈ π‘ˆ)
36 df-ss 3964 . . . . . . . . . . . . . 14 (𝑀 βŠ† (𝐴 Γ— 𝐴) ↔ (𝑀 ∩ (𝐴 Γ— 𝐴)) = 𝑀)
3724, 36sylib 217 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 ∩ (𝐴 Γ— 𝐴)) = 𝑀)
3837uneq1d 4161 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))))
39 simpr 486 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
40 simpllr 775 . . . . . . . . . . . . . 14 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 βŠ† 𝑀)
4139, 40eqsstrrd 4020 . . . . . . . . . . . . 13 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑒 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑀)
42 ssequn2 4182 . . . . . . . . . . . . 13 ((𝑒 ∩ (𝐴 Γ— 𝐴)) βŠ† 𝑀 ↔ (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = 𝑀)
4341, 42sylib 217 . . . . . . . . . . . 12 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑀 βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))) = 𝑀)
4438, 43eqtr2d 2774 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 = ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴))))
45 indir 4274 . . . . . . . . . . 11 ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)) = ((𝑀 ∩ (𝐴 Γ— 𝐴)) βˆͺ (𝑒 ∩ (𝐴 Γ— 𝐴)))
4644, 45eqtr4di 2791 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)))
47 ineq1 4204 . . . . . . . . . . 11 (π‘₯ = (𝑀 βˆͺ 𝑒) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴)))
4847rspceeqv 3632 . . . . . . . . . 10 (((𝑀 βˆͺ 𝑒) ∈ π‘ˆ ∧ 𝑀 = ((𝑀 βˆͺ 𝑒) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
4935, 46, 48syl2anc 585 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
50 elrest 17369 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
5150biimpar 479 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
5220, 21, 49, 51syl21anc 837 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
53 elrest 17369 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))))
5453biimpa 478 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5514, 54syldanl 603 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5655ad2antrr 725 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
5752, 56r19.29a 3163 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) ∧ 𝑣 βŠ† 𝑀) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
5857ex 414 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ 𝒫 (𝐴 Γ— 𝐴)) β†’ (𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))))
5958ralrimiva 3147 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))))
609ad5antr 733 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
6114ad5antr 733 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝐴 Γ— 𝐴) ∈ V)
62 simpllr 775 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑒 ∈ π‘ˆ)
63 simplr 768 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ π‘₯ ∈ π‘ˆ)
64 ustincl 23694 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ ∧ π‘₯ ∈ π‘ˆ) β†’ (𝑒 ∩ π‘₯) ∈ π‘ˆ)
6560, 62, 63, 64syl3anc 1372 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑒 ∩ π‘₯) ∈ π‘ˆ)
66 simprl 770 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
67 simprr 772 . . . . . . . . . . 11 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
6866, 67ineq12d 4212 . . . . . . . . . 10 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) ∩ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
69 inindir 4226 . . . . . . . . . 10 ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ (𝐴 Γ— 𝐴)) ∩ (π‘₯ ∩ (𝐴 Γ— 𝐴)))
7068, 69eqtr4di 2791 . . . . . . . . 9 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)))
71 ineq1 4204 . . . . . . . . . 10 (𝑦 = (𝑒 ∩ π‘₯) β†’ (𝑦 ∩ (𝐴 Γ— 𝐴)) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴)))
7271rspceeqv 3632 . . . . . . . . 9 (((𝑒 ∩ π‘₯) ∈ π‘ˆ ∧ (𝑣 ∩ 𝑀) = ((𝑒 ∩ π‘₯) ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴)))
7365, 70, 72syl2anc 585 . . . . . . . 8 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴)))
74 elrest 17369 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ ((𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴))))
7574biimpar 479 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘¦ ∈ π‘ˆ (𝑣 ∩ 𝑀) = (𝑦 ∩ (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
7660, 61, 73, 75syl21anc 837 . . . . . . 7 (((((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
7755adantr 482 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
789ad2antrr 725 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
7914ad2antrr 725 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
80 simpr 486 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
8150biimpa 478 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
8278, 79, 80, 81syl21anc 837 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
83 reeanv 3227 . . . . . . . 8 (βˆƒπ‘’ ∈ π‘ˆ βˆƒπ‘₯ ∈ π‘ˆ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) ↔ (βˆƒπ‘’ ∈ π‘ˆ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘₯ ∈ π‘ˆ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
8477, 82, 83sylanbrc 584 . . . . . . 7 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘’ ∈ π‘ˆ βˆƒπ‘₯ ∈ π‘ˆ (𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)) ∧ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
8576, 84r19.29vva 3214 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
8685ralrimiva 3147 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
87 simp-4l 782 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
88 simplr 768 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑒 ∈ π‘ˆ)
89 ustdiag 23695 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ ( I β†Ύ 𝑋) βŠ† 𝑒)
9087, 88, 89syl2anc 585 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝑋) βŠ† 𝑒)
91 simp-4r 783 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝐴 βŠ† 𝑋)
92 inss1 4227 . . . . . . . . . . . . . 14 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† ( I β†Ύ 𝑋)
93 resss 6004 . . . . . . . . . . . . . 14 ( I β†Ύ 𝑋) βŠ† I
9492, 93sstri 3990 . . . . . . . . . . . . 13 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† I
95 iss 6033 . . . . . . . . . . . . 13 ((( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† I ↔ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴))))
9694, 95mpbi 229 . . . . . . . . . . . 12 (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
97 simpr 486 . . . . . . . . . . . . . . . 16 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝐴)
98 ssel2 3976 . . . . . . . . . . . . . . . . 17 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒 ∈ 𝑋)
99 equid 2016 . . . . . . . . . . . . . . . . . 18 𝑒 = 𝑒
100 resieq 5990 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ 𝑋 ∧ 𝑒 ∈ 𝑋) β†’ (𝑒( I β†Ύ 𝑋)𝑒 ↔ 𝑒 = 𝑒))
10199, 100mpbiri 258 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ 𝑋 ∧ 𝑒 ∈ 𝑋) β†’ 𝑒( I β†Ύ 𝑋)𝑒)
10298, 98, 101syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ 𝑒( I β†Ύ 𝑋)𝑒)
103 breq2 5151 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑒 β†’ (𝑒( I β†Ύ 𝑋)𝑣 ↔ 𝑒( I β†Ύ 𝑋)𝑒))
104103rspcev 3612 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ 𝐴 ∧ 𝑒( I β†Ύ 𝑋)𝑒) β†’ βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
10597, 102, 104syl2anc 585 . . . . . . . . . . . . . . 15 ((𝐴 βŠ† 𝑋 ∧ 𝑒 ∈ 𝐴) β†’ βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
106105ralrimiva 3147 . . . . . . . . . . . . . 14 (𝐴 βŠ† 𝑋 β†’ βˆ€π‘’ ∈ 𝐴 βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
107 dminxp 6176 . . . . . . . . . . . . . 14 (dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = 𝐴 ↔ βˆ€π‘’ ∈ 𝐴 βˆƒπ‘£ ∈ 𝐴 𝑒( I β†Ύ 𝑋)𝑣)
108106, 107sylibr 233 . . . . . . . . . . . . 13 (𝐴 βŠ† 𝑋 β†’ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) = 𝐴)
109108reseq2d 5979 . . . . . . . . . . . 12 (𝐴 βŠ† 𝑋 β†’ ( I β†Ύ dom (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴))) = ( I β†Ύ 𝐴))
11096, 109eqtr2id 2786 . . . . . . . . . . 11 (𝐴 βŠ† 𝑋 β†’ ( I β†Ύ 𝐴) = (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
111110adantl 483 . . . . . . . . . 10 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ ( I β†Ύ 𝐴) = (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)))
112 ssrin 4232 . . . . . . . . . . 11 (( I β†Ύ 𝑋) βŠ† 𝑒 β†’ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
113112adantr 482 . . . . . . . . . 10 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ (( I β†Ύ 𝑋) ∩ (𝐴 Γ— 𝐴)) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
114111, 113eqsstrd 4019 . . . . . . . . 9 ((( I β†Ύ 𝑋) βŠ† 𝑒 ∧ 𝐴 βŠ† 𝑋) β†’ ( I β†Ύ 𝐴) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
11590, 91, 114syl2anc 585 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
116 simpr 486 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴)))
117115, 116sseqtrrd 4022 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† 𝑣)
118117, 55r19.29a 3163 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ ( I β†Ύ 𝐴) βŠ† 𝑣)
11914ad3antrrr 729 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (𝐴 Γ— 𝐴) ∈ V)
120 ustinvel 23696 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ ◑𝑒 ∈ π‘ˆ)
12187, 88, 120syl2anc 585 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑒 ∈ π‘ˆ)
122116cnveqd 5873 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 = β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)))
123 cnvin 6141 . . . . . . . . . . 11 β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ β—‘(𝐴 Γ— 𝐴))
124 cnvxp 6153 . . . . . . . . . . . 12 β—‘(𝐴 Γ— 𝐴) = (𝐴 Γ— 𝐴)
125124ineq2i 4208 . . . . . . . . . . 11 (◑𝑒 ∩ β—‘(𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴))
126123, 125eqtri 2761 . . . . . . . . . 10 β—‘(𝑒 ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴))
127122, 126eqtrdi 2789 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 = (◑𝑒 ∩ (𝐴 Γ— 𝐴)))
128 ineq1 4204 . . . . . . . . . 10 (π‘₯ = ◑𝑒 β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) = (◑𝑒 ∩ (𝐴 Γ— 𝐴)))
129128rspceeqv 3632 . . . . . . . . 9 ((◑𝑒 ∈ π‘ˆ ∧ ◑𝑣 = (◑𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
130121, 127, 129syl2anc 585 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
131 elrest 17369 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) β†’ (◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ↔ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴))))
132131biimpar 479 . . . . . . . 8 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V) ∧ βˆƒπ‘₯ ∈ π‘ˆ ◑𝑣 = (π‘₯ ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
13387, 119, 130, 132syl21anc 837 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
134133, 55r19.29a 3163 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
135 simp-4l 782 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
13614ad3antrrr 729 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ (𝐴 Γ— 𝐴) ∈ V)
137 simplr 768 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ π‘₯ ∈ π‘ˆ)
138 elrestr 17370 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ (𝐴 Γ— 𝐴) ∈ V ∧ π‘₯ ∈ π‘ˆ) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
139135, 136, 137, 138syl3anc 1372 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ (π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)))
140 inss1 4227 . . . . . . . . . . . . . . 15 (π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯
141 coss1 5853 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
142 coss2 5854 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ (π‘₯ ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯))
143141, 142sstrd 3991 . . . . . . . . . . . . . . 15 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† π‘₯ β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯))
144140, 143ax-mp 5 . . . . . . . . . . . . . 14 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯)
145 sstr 3989 . . . . . . . . . . . . . 14 ((((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (π‘₯ ∘ π‘₯) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
146144, 145mpan 689 . . . . . . . . . . . . 13 ((π‘₯ ∘ π‘₯) βŠ† 𝑒 β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
147146adantl 483 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† 𝑒)
148 inss2 4228 . . . . . . . . . . . . . . 15 (π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
149 coss1 5853 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
150 coss2 5854 . . . . . . . . . . . . . . . 16 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((𝐴 Γ— 𝐴) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)))
151149, 150sstrd 3991 . . . . . . . . . . . . . . 15 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)))
152148, 151ax-mp 5 . . . . . . . . . . . . . 14 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴))
153 xpidtr 6120 . . . . . . . . . . . . . 14 ((𝐴 Γ— 𝐴) ∘ (𝐴 Γ— 𝐴)) βŠ† (𝐴 Γ— 𝐴)
154152, 153sstri 3990 . . . . . . . . . . . . 13 ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝐴 Γ— 𝐴)
155154a1i 11 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝐴 Γ— 𝐴))
156147, 155ssind 4231 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
157 id 22 . . . . . . . . . . . . . 14 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ 𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)))
158157, 157coeq12d 5862 . . . . . . . . . . . . 13 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ (𝑀 ∘ 𝑀) = ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))))
159158sseq1d 4012 . . . . . . . . . . . 12 (𝑀 = (π‘₯ ∩ (𝐴 Γ— 𝐴)) β†’ ((𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)) ↔ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
160159rspcev 3612 . . . . . . . . . . 11 (((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ ((π‘₯ ∩ (𝐴 Γ— 𝐴)) ∘ (π‘₯ ∩ (𝐴 Γ— 𝐴))) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
161139, 156, 160syl2anc 585 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) ∧ π‘₯ ∈ π‘ˆ) ∧ (π‘₯ ∘ π‘₯) βŠ† 𝑒) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
162 ustexhalf 23697 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘₯ ∈ π‘ˆ (π‘₯ ∘ π‘₯) βŠ† 𝑒)
163162adantlr 714 . . . . . . . . . 10 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘₯ ∈ π‘ˆ (π‘₯ ∘ π‘₯) βŠ† 𝑒)
164161, 163r19.29a 3163 . . . . . . . . 9 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑒 ∈ π‘ˆ) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
165164ad4ant13 750 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴)))
166116sseq2d 4013 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ ((𝑀 ∘ 𝑀) βŠ† 𝑣 ↔ (𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
167166rexbidv 3179 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ (βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣 ↔ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† (𝑒 ∩ (𝐴 Γ— 𝐴))))
168165, 167mpbird 257 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ 𝑒 ∈ π‘ˆ) ∧ 𝑣 = (𝑒 ∩ (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)
169168, 55r19.29a 3163 . . . . . 6 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)
170118, 134, 1693jca 1129 . . . . 5 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣))
17159, 86, 1703jca 1129 . . . 4 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) ∧ 𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) β†’ (βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))
172171ralrimiva 3147 . . 3 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣)))
1732, 19, 1723jca 1129 . 2 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝐴 βŠ† 𝑋) β†’ ((π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) βŠ† 𝒫 (𝐴 Γ— 𝐴) ∧ (𝐴 Γ— 𝐴) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆ€π‘£ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(βˆ€π‘€ ∈ 𝒫 (𝐴 Γ— 𝐴)(𝑣 βŠ† 𝑀 β†’ 𝑀 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))) ∧ βˆ€π‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑣 ∩ 𝑀) ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ (( I β†Ύ 𝐴) βŠ† 𝑣 ∧ ◑𝑣 ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴)) ∧ βˆƒπ‘€ ∈ (π‘ˆ β†Ύt (𝐴 Γ— 𝐴))(𝑀 ∘ 𝑀) βŠ† 𝑣))))
174 isust 23690 . . 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 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  π’« cpw 4601   class class class wbr 5147   I cid 5572   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675   β†Ύ cres 5677   ∘ ccom 5679  β€˜cfv 6540  (class class class)co 7404   β†Ύt crest 17362  UnifOncust 23686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-1st 7970  df-2nd 7971  df-rest 17364  df-ust 23687
This theorem is referenced by:  restutop  23724  restutopopn  23725  ressust  23750  ressusp  23751  trcfilu  23781  cfiluweak  23782
  Copyright terms: Public domain W3C validator