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

Theorem trust 22931
 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 16764 . . . 4 (𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
21a1i 11 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3 inxp 5673 . . . . . 6 ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋𝐴) × (𝑋𝐴))
4 sseqin2 4121 . . . . . . . 8 (𝐴𝑋 ↔ (𝑋𝐴) = 𝐴)
54biimpi 219 . . . . . . 7 (𝐴𝑋 → (𝑋𝐴) = 𝐴)
65sqxpeqd 5557 . . . . . 6 (𝐴𝑋 → ((𝑋𝐴) × (𝑋𝐴)) = (𝐴 × 𝐴))
73, 6syl5eq 2806 . . . . 5 (𝐴𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
87adantl 486 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9 simpl 487 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10 elfvex 6692 . . . . . . . 8 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
1110adantr 485 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝑋 ∈ V)
12 simpr 489 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝐴𝑋)
1311, 12ssexd 5195 . . . . . 6 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝐴 ∈ V)
1413, 13xpexd 7473 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝐴 × 𝐴) ∈ V)
15 ustbasel 22908 . . . . . 6 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
1615adantr 485 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
17 elrestr 16761 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
189, 14, 16, 17syl3anc 1369 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
198, 18eqeltrrd 2854 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)))
209ad5antr 734 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
2114ad5antr 734 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
22 simplr 769 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
23 simp-4r 784 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
2423elpwid 4506 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
2512ad5antr 734 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴𝑋)
26 xpss12 5540 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐴𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
2725, 25, 26syl2anc 588 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
2824, 27sstrd 3903 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
29 ustssxp 22906 . . . . . . . . . . . . 13 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
3020, 22, 29syl2anc 588 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
3128, 30unssd 4092 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤𝑢) ⊆ (𝑋 × 𝑋))
32 ssun2 4079 . . . . . . . . . . . 12 𝑢 ⊆ (𝑤𝑢)
33 ustssel 22907 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈 ∧ (𝑤𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤𝑢) → (𝑤𝑢) ∈ 𝑈))
3432, 33mpi 20 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈 ∧ (𝑤𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤𝑢) ∈ 𝑈)
3520, 22, 31, 34syl3anc 1369 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤𝑢) ∈ 𝑈)
36 df-ss 3876 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
3724, 36sylib 221 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
3837uneq1d 4068 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
39 simpr 489 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
40 simpllr 776 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣𝑤)
4139, 40eqsstrrd 3932 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
42 ssequn2 4089 . . . . . . . . . . . . 13 ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
4341, 42sylib 221 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
4438, 43eqtr2d 2795 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
45 indir 4181 . . . . . . . . . . 11 ((𝑤𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
4644, 45eqtr4di 2812 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤𝑢) ∩ (𝐴 × 𝐴)))
47 ineq1 4110 . . . . . . . . . . 11 (𝑥 = (𝑤𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤𝑢) ∩ (𝐴 × 𝐴)))
4847rspceeqv 3557 . . . . . . . . . 10 (((𝑤𝑢) ∈ 𝑈𝑤 = ((𝑤𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
4935, 46, 48syl2anc 588 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
50 elrest 16760 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
5150biimpar 482 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
5220, 21, 49, 51syl21anc 837 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
53 elrest 16760 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
5453biimpa 481 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5514, 54syldanl 605 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5655ad2antrr 726 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5752, 56r19.29a 3214 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
5857ex 417 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))))
5958ralrimiva 3114 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))))
609ad5antr 734 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
6114ad5antr 734 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
62 simpllr 776 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢𝑈)
63 simplr 769 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥𝑈)
64 ustincl 22909 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑥𝑈) → (𝑢𝑥) ∈ 𝑈)
6560, 62, 63, 64syl3anc 1369 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢𝑥) ∈ 𝑈)
66 simprl 771 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
67 simprr 773 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
6866, 67ineq12d 4119 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
69 inindir 4133 . . . . . . . . . 10 ((𝑢𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
7068, 69eqtr4di 2812 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) = ((𝑢𝑥) ∩ (𝐴 × 𝐴)))
71 ineq1 4110 . . . . . . . . . 10 (𝑦 = (𝑢𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢𝑥) ∩ (𝐴 × 𝐴)))
7271rspceeqv 3557 . . . . . . . . 9 (((𝑢𝑥) ∈ 𝑈 ∧ (𝑣𝑤) = ((𝑢𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
7365, 70, 72syl2anc 588 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
74 elrest 16760 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
7574biimpar 482 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
7660, 61, 73, 75syl21anc 837 . . . . . . 7 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
7755adantr 485 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
789ad2antrr 726 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
7914ad2antrr 726 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
80 simpr 489 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
8150biimpa 481 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
8278, 79, 80, 81syl21anc 837 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
83 reeanv 3286 . . . . . . . 8 (∃𝑢𝑈𝑥𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
8477, 82, 83sylanbrc 587 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈𝑥𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
8576, 84r19.29vva 3258 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
8685ralrimiva 3114 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
87 simp-4l 783 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
88 simplr 769 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
89 ustdiag 22910 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
9087, 88, 89syl2anc 588 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
91 simp-4r 784 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴𝑋)
92 inss1 4134 . . . . . . . . . . . . . 14 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
93 resss 5849 . . . . . . . . . . . . . 14 ( I ↾ 𝑋) ⊆ I
9492, 93sstri 3902 . . . . . . . . . . . . 13 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
95 iss 5876 . . . . . . . . . . . . 13 ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
9694, 95mpbi 233 . . . . . . . . . . . 12 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
97 simpr 489 . . . . . . . . . . . . . . . 16 ((𝐴𝑋𝑢𝐴) → 𝑢𝐴)
98 ssel2 3888 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋𝑢𝐴) → 𝑢𝑋)
99 equid 2020 . . . . . . . . . . . . . . . . . 18 𝑢 = 𝑢
100 resieq 5835 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑋𝑢𝑋) → (𝑢( I ↾ 𝑋)𝑢𝑢 = 𝑢))
10199, 100mpbiri 261 . . . . . . . . . . . . . . . . 17 ((𝑢𝑋𝑢𝑋) → 𝑢( I ↾ 𝑋)𝑢)
10298, 98, 101syl2anc 588 . . . . . . . . . . . . . . . 16 ((𝐴𝑋𝑢𝐴) → 𝑢( I ↾ 𝑋)𝑢)
103 breq2 5037 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣𝑢( I ↾ 𝑋)𝑢))
104103rspcev 3542 . . . . . . . . . . . . . . . 16 ((𝑢𝐴𝑢( I ↾ 𝑋)𝑢) → ∃𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
10597, 102, 104syl2anc 588 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝑢𝐴) → ∃𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
106105ralrimiva 3114 . . . . . . . . . . . . . 14 (𝐴𝑋 → ∀𝑢𝐴𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
107 dminxp 6010 . . . . . . . . . . . . . 14 (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢𝐴𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
108106, 107sylibr 237 . . . . . . . . . . . . 13 (𝐴𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
109108reseq2d 5824 . . . . . . . . . . . 12 (𝐴𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
11096, 109syl5req 2807 . . . . . . . . . . 11 (𝐴𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
111110adantl 486 . . . . . . . . . 10 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112 ssrin 4139 . . . . . . . . . . 11 (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
113112adantr 485 . . . . . . . . . 10 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114111, 113eqsstrd 3931 . . . . . . . . 9 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
11590, 91, 114syl2anc 588 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
116 simpr 489 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
117115, 116sseqtrrd 3934 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
118117, 55r19.29a 3214 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
11914ad3antrrr 730 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
120 ustinvel 22911 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → 𝑢𝑈)
12187, 88, 120syl2anc 588 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
122116cnveqd 5716 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
123 cnvin 5976 . . . . . . . . . . 11 (𝑢 ∩ (𝐴 × 𝐴)) = (𝑢(𝐴 × 𝐴))
124 cnvxp 5987 . . . . . . . . . . . 12 (𝐴 × 𝐴) = (𝐴 × 𝐴)
125124ineq2i 4115 . . . . . . . . . . 11 (𝑢(𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
126123, 125eqtri 2782 . . . . . . . . . 10 (𝑢 ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
127122, 126eqtrdi 2810 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
128 ineq1 4110 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴)))
129128rspceeqv 3557 . . . . . . . . 9 ((𝑢𝑈𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
130121, 127, 129syl2anc 588 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131 elrest 16760 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
132131biimpar 482 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
13387, 119, 130, 132syl21anc 837 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
134133, 55r19.29a 3214 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
135 simp-4l 783 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
13614ad3antrrr 730 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
137 simplr 769 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → 𝑥𝑈)
138 elrestr 16761 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
139135, 136, 137, 138syl3anc 1369 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
140 inss1 4134 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
141 coss1 5696 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
142 coss2 5697 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥))
143141, 142sstrd 3903 . . . . . . . . . . . . . . 15 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥))
144140, 143ax-mp 5 . . . . . . . . . . . . . 14 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥)
145 sstr 3901 . . . . . . . . . . . . . 14 ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
146144, 145mpan 690 . . . . . . . . . . . . 13 ((𝑥𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147146adantl 486 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148 inss2 4135 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
149 coss1 5696 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
150 coss2 5697 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
151149, 150sstrd 3903 . . . . . . . . . . . . . . 15 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152148, 151ax-mp 5 . . . . . . . . . . . . . 14 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
153 xpidtr 5955 . . . . . . . . . . . . . 14 ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
154152, 153sstri 3902 . . . . . . . . . . . . 13 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
155154a1i 11 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
156147, 155ssind 4138 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
157 id 22 . . . . . . . . . . . . . 14 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
158157, 157coeq12d 5705 . . . . . . . . . . . . 13 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
159158sseq1d 3924 . . . . . . . . . . . 12 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
160159rspcev 3542 . . . . . . . . . . 11 (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
161139, 156, 160syl2anc 588 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162 ustexhalf 22912 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → ∃𝑥𝑈 (𝑥𝑥) ⊆ 𝑢)
163162adantlr 715 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) → ∃𝑥𝑈 (𝑥𝑥) ⊆ 𝑢)
164161, 163r19.29a 3214 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
165164ad4ant13 751 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166116sseq2d 3925 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤𝑤) ⊆ 𝑣 ↔ (𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
167166rexbidv 3222 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168165, 167mpbird 260 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)
169168, 55r19.29a 3214 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)
170118, 134, 1693jca 1126 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣))
17159, 86, 1703jca 1126 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))
172171ralrimiva 3114 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))
1732, 19, 1723jca 1126 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣))))
174 isust 22905 . . 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 260 1 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  Vcvv 3410   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  𝒫 cpw 4495   class class class wbr 5033   I cid 5430   × cxp 5523  ◡ccnv 5524  dom cdm 5525   ↾ cres 5527   ∘ ccom 5529  ‘cfv 6336  (class class class)co 7151   ↾t crest 16753  UnifOncust 22901 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-1st 7694  df-2nd 7695  df-rest 16755  df-ust 22902 This theorem is referenced by:  restutop  22939  restutopopn  22940  ressust  22966  ressusp  22967  trcfilu  22996  cfiluweak  22997
 Copyright terms: Public domain W3C validator