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

Theorem trust 22312
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 16360 . . . 4 (𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴)
21a1i 11 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴))
3 inxp 5423 . . . . . 6 ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = ((𝑋𝐴) × (𝑋𝐴))
4 sseqin2 3979 . . . . . . . 8 (𝐴𝑋 ↔ (𝑋𝐴) = 𝐴)
54biimpi 207 . . . . . . 7 (𝐴𝑋 → (𝑋𝐴) = 𝐴)
65sqxpeqd 5309 . . . . . 6 (𝐴𝑋 → ((𝑋𝐴) × (𝑋𝐴)) = (𝐴 × 𝐴))
73, 6syl5eq 2811 . . . . 5 (𝐴𝑋 → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
87adantl 473 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) = (𝐴 × 𝐴))
9 simpl 474 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
10 elfvex 6409 . . . . . . . 8 (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ V)
1110adantr 472 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝑋 ∈ V)
12 simpr 477 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝐴𝑋)
1311, 12ssexd 4966 . . . . . 6 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → 𝐴 ∈ V)
14 xpexg 7158 . . . . . 6 ((𝐴 ∈ V ∧ 𝐴 ∈ V) → (𝐴 × 𝐴) ∈ V)
1513, 13, 14syl2anc 579 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝐴 × 𝐴) ∈ V)
16 ustbasel 22289 . . . . . 6 (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
1716adantr 472 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑋 × 𝑋) ∈ 𝑈)
18 elrestr 16357 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ (𝑋 × 𝑋) ∈ 𝑈) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
199, 15, 17, 18syl3anc 1490 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑋 × 𝑋) ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
208, 19eqeltrrd 2845 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)))
219ad5antr 728 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
2215ad5antr 728 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
23 simplr 785 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
24 simp-4r 803 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ 𝒫 (𝐴 × 𝐴))
2524elpwid 4327 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝐴 × 𝐴))
2612ad5antr 728 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴𝑋)
27 xpss12 5292 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐴𝑋) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
2826, 26, 27syl2anc 579 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ⊆ (𝑋 × 𝑋))
2925, 28sstrd 3771 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ⊆ (𝑋 × 𝑋))
30 ustssxp 22287 . . . . . . . . . . . . 13 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → 𝑢 ⊆ (𝑋 × 𝑋))
3121, 23, 30syl2anc 579 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢 ⊆ (𝑋 × 𝑋))
3229, 31unssd 3951 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤𝑢) ⊆ (𝑋 × 𝑋))
33 ssun2 3939 . . . . . . . . . . . 12 𝑢 ⊆ (𝑤𝑢)
34 ustssel 22288 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈 ∧ (𝑤𝑢) ⊆ (𝑋 × 𝑋)) → (𝑢 ⊆ (𝑤𝑢) → (𝑤𝑢) ∈ 𝑈))
3533, 34mpi 20 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈 ∧ (𝑤𝑢) ⊆ (𝑋 × 𝑋)) → (𝑤𝑢) ∈ 𝑈)
3621, 23, 32, 35syl3anc 1490 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤𝑢) ∈ 𝑈)
37 df-ss 3746 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐴 × 𝐴) ↔ (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
3825, 37sylib 209 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∩ (𝐴 × 𝐴)) = 𝑤)
3938uneq1d 3928 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))) = (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))))
40 simpr 477 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
41 simpllr 793 . . . . . . . . . . . . . 14 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣𝑤)
4240, 41eqsstr3d 3800 . . . . . . . . . . . . 13 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤)
43 ssequn2 3948 . . . . . . . . . . . . 13 ((𝑢 ∩ (𝐴 × 𝐴)) ⊆ 𝑤 ↔ (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
4442, 43sylib 209 . . . . . . . . . . . 12 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝑤 ∪ (𝑢 ∩ (𝐴 × 𝐴))) = 𝑤)
4539, 44eqtr2d 2800 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴))))
46 indir 4040 . . . . . . . . . . 11 ((𝑤𝑢) ∩ (𝐴 × 𝐴)) = ((𝑤 ∩ (𝐴 × 𝐴)) ∪ (𝑢 ∩ (𝐴 × 𝐴)))
4745, 46syl6eqr 2817 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 = ((𝑤𝑢) ∩ (𝐴 × 𝐴)))
48 ineq1 3969 . . . . . . . . . . 11 (𝑥 = (𝑤𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) = ((𝑤𝑢) ∩ (𝐴 × 𝐴)))
4948rspceeqv 3479 . . . . . . . . . 10 (((𝑤𝑢) ∈ 𝑈𝑤 = ((𝑤𝑢) ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
5036, 47, 49syl2anc 579 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
51 elrest 16356 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑤 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
5251biimpar 469 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
5321, 22, 50, 52syl21anc 866 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
54 elrest 16356 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))))
5554biimpa 468 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5615, 55syldanl 595 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5756ad2antrr 717 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
5853, 57r19.29a 3225 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) ∧ 𝑣𝑤) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
5958ex 401 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ 𝒫 (𝐴 × 𝐴)) → (𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))))
6059ralrimiva 3113 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))))
619ad5antr 728 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑈 ∈ (UnifOn‘𝑋))
6215ad5antr 728 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝐴 × 𝐴) ∈ V)
63 simpllr 793 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑢𝑈)
64 simplr 785 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑥𝑈)
65 ustincl 22290 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈𝑥𝑈) → (𝑢𝑥) ∈ 𝑈)
6661, 63, 64, 65syl3anc 1490 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑢𝑥) ∈ 𝑈)
67 simprl 787 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
68 simprr 789 . . . . . . . . . . 11 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
6967, 68ineq12d 3977 . . . . . . . . . 10 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴))))
70 inindir 3991 . . . . . . . . . 10 ((𝑢𝑥) ∩ (𝐴 × 𝐴)) = ((𝑢 ∩ (𝐴 × 𝐴)) ∩ (𝑥 ∩ (𝐴 × 𝐴)))
7169, 70syl6eqr 2817 . . . . . . . . 9 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) = ((𝑢𝑥) ∩ (𝐴 × 𝐴)))
72 ineq1 3969 . . . . . . . . . 10 (𝑦 = (𝑢𝑥) → (𝑦 ∩ (𝐴 × 𝐴)) = ((𝑢𝑥) ∩ (𝐴 × 𝐴)))
7372rspceeqv 3479 . . . . . . . . 9 (((𝑢𝑥) ∈ 𝑈 ∧ (𝑣𝑤) = ((𝑢𝑥) ∩ (𝐴 × 𝐴))) → ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
7466, 71, 73syl2anc 579 . . . . . . . 8 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴)))
75 elrest 16356 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → ((𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴))))
7675biimpar 469 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑦𝑈 (𝑣𝑤) = (𝑦 ∩ (𝐴 × 𝐴))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
7761, 62, 74, 76syl21anc 866 . . . . . . 7 (((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
7856adantr 472 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
799ad2antrr 717 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
8015ad2antrr 717 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
81 simpr 477 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑤 ∈ (𝑈t (𝐴 × 𝐴)))
8251biimpa 468 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
8379, 80, 81, 82syl21anc 866 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
84 reeanv 3254 . . . . . . . 8 (∃𝑢𝑈𝑥𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))) ↔ (∃𝑢𝑈 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ ∃𝑥𝑈 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
8578, 83, 84sylanbrc 578 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑢𝑈𝑥𝑈 (𝑣 = (𝑢 ∩ (𝐴 × 𝐴)) ∧ 𝑤 = (𝑥 ∩ (𝐴 × 𝐴))))
8677, 85r19.29vva 3228 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑤 ∈ (𝑈t (𝐴 × 𝐴))) → (𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
8786ralrimiva 3113 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)))
88 simp-4l 801 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑈 ∈ (UnifOn‘𝑋))
89 simplr 785 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
90 ustdiag 22291 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → ( I ↾ 𝑋) ⊆ 𝑢)
9188, 89, 90syl2anc 579 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝑋) ⊆ 𝑢)
92 simp-4r 803 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝐴𝑋)
93 inss1 3992 . . . . . . . . . . . . . 14 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ ( I ↾ 𝑋)
94 resss 5597 . . . . . . . . . . . . . 14 ( I ↾ 𝑋) ⊆ I
9593, 94sstri 3770 . . . . . . . . . . . . 13 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I
96 iss 5624 . . . . . . . . . . . . 13 ((( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ I ↔ (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))))
9795, 96mpbi 221 . . . . . . . . . . . 12 (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
98 simpr 477 . . . . . . . . . . . . . . . 16 ((𝐴𝑋𝑢𝐴) → 𝑢𝐴)
99 ssel2 3756 . . . . . . . . . . . . . . . . 17 ((𝐴𝑋𝑢𝐴) → 𝑢𝑋)
100 equid 2109 . . . . . . . . . . . . . . . . . 18 𝑢 = 𝑢
101 resieq 5583 . . . . . . . . . . . . . . . . . 18 ((𝑢𝑋𝑢𝑋) → (𝑢( I ↾ 𝑋)𝑢𝑢 = 𝑢))
102100, 101mpbiri 249 . . . . . . . . . . . . . . . . 17 ((𝑢𝑋𝑢𝑋) → 𝑢( I ↾ 𝑋)𝑢)
10399, 99, 102syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝐴𝑋𝑢𝐴) → 𝑢( I ↾ 𝑋)𝑢)
104 breq2 4813 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑢 → (𝑢( I ↾ 𝑋)𝑣𝑢( I ↾ 𝑋)𝑢))
105104rspcev 3461 . . . . . . . . . . . . . . . 16 ((𝑢𝐴𝑢( I ↾ 𝑋)𝑢) → ∃𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
10698, 103, 105syl2anc 579 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝑢𝐴) → ∃𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
107106ralrimiva 3113 . . . . . . . . . . . . . 14 (𝐴𝑋 → ∀𝑢𝐴𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
108 dminxp 5757 . . . . . . . . . . . . . 14 (dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴 ↔ ∀𝑢𝐴𝑣𝐴 𝑢( I ↾ 𝑋)𝑣)
109107, 108sylibr 225 . . . . . . . . . . . . 13 (𝐴𝑋 → dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) = 𝐴)
110109reseq2d 5565 . . . . . . . . . . . 12 (𝐴𝑋 → ( I ↾ dom (( I ↾ 𝑋) ∩ (𝐴 × 𝐴))) = ( I ↾ 𝐴))
11197, 110syl5req 2812 . . . . . . . . . . 11 (𝐴𝑋 → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
112111adantl 473 . . . . . . . . . 10 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → ( I ↾ 𝐴) = (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)))
113 ssrin 3997 . . . . . . . . . . 11 (( I ↾ 𝑋) ⊆ 𝑢 → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
114113adantr 472 . . . . . . . . . 10 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → (( I ↾ 𝑋) ∩ (𝐴 × 𝐴)) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
115112, 114eqsstrd 3799 . . . . . . . . 9 ((( I ↾ 𝑋) ⊆ 𝑢𝐴𝑋) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
11691, 92, 115syl2anc 579 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
117 simpr 477 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
118116, 117sseqtr4d 3802 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
119118, 56r19.29a 3225 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ( I ↾ 𝐴) ⊆ 𝑣)
12015ad3antrrr 721 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (𝐴 × 𝐴) ∈ V)
121 ustinvel 22292 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → 𝑢𝑈)
12288, 89, 121syl2anc 579 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑢𝑈)
123117cnveqd 5466 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
124 cnvin 5723 . . . . . . . . . . 11 (𝑢 ∩ (𝐴 × 𝐴)) = (𝑢(𝐴 × 𝐴))
125 cnvxp 5734 . . . . . . . . . . . 12 (𝐴 × 𝐴) = (𝐴 × 𝐴)
126125ineq2i 3973 . . . . . . . . . . 11 (𝑢(𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
127124, 126eqtri 2787 . . . . . . . . . 10 (𝑢 ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴))
128123, 127syl6eq 2815 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 = (𝑢 ∩ (𝐴 × 𝐴)))
129 ineq1 3969 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑥 ∩ (𝐴 × 𝐴)) = (𝑢 ∩ (𝐴 × 𝐴)))
130129rspceeqv 3479 . . . . . . . . 9 ((𝑢𝑈𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
131122, 128, 130syl2anc 579 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴)))
132 elrest 16356 . . . . . . . . 9 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) → (𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ↔ ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴))))
133132biimpar 469 . . . . . . . 8 (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V) ∧ ∃𝑥𝑈 𝑣 = (𝑥 ∩ (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
13488, 120, 131, 133syl21anc 866 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
135134, 56r19.29a 3225 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → 𝑣 ∈ (𝑈t (𝐴 × 𝐴)))
136 simp-4l 801 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → 𝑈 ∈ (UnifOn‘𝑋))
13715ad3antrrr 721 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → (𝐴 × 𝐴) ∈ V)
138 simplr 785 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → 𝑥𝑈)
139 elrestr 16357 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝐴 × 𝐴) ∈ V ∧ 𝑥𝑈) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
140136, 137, 138, 139syl3anc 1490 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → (𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)))
141 inss1 3992 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥
142 coss1 5446 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))))
143 coss2 5447 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → (𝑥 ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥))
144142, 143sstrd 3771 . . . . . . . . . . . . . . 15 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ 𝑥 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥))
145141, 144ax-mp 5 . . . . . . . . . . . . . 14 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥)
146 sstr 3769 . . . . . . . . . . . . . 14 ((((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑥𝑥) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
147145, 146mpan 681 . . . . . . . . . . . . 13 ((𝑥𝑥) ⊆ 𝑢 → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
148147adantl 473 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ 𝑢)
149 inss2 3993 . . . . . . . . . . . . . . 15 (𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
150 coss1 5446 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
151 coss2 5447 . . . . . . . . . . . . . . . 16 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝐴 × 𝐴) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
152150, 151sstrd 3771 . . . . . . . . . . . . . . 15 ((𝑥 ∩ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)))
153149, 152ax-mp 5 . . . . . . . . . . . . . 14 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴))
154 xpidtr 5701 . . . . . . . . . . . . . 14 ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴)
155153, 154sstri 3770 . . . . . . . . . . . . 13 ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴)
156155a1i 11 . . . . . . . . . . . 12 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝐴 × 𝐴))
157148, 156ssind 3996 . . . . . . . . . . 11 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
158 id 22 . . . . . . . . . . . . . 14 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → 𝑤 = (𝑥 ∩ (𝐴 × 𝐴)))
159158, 158coeq12d 5455 . . . . . . . . . . . . 13 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → (𝑤𝑤) = ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))))
160159sseq1d 3792 . . . . . . . . . . . 12 (𝑤 = (𝑥 ∩ (𝐴 × 𝐴)) → ((𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)) ↔ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
161160rspcev 3461 . . . . . . . . . . 11 (((𝑥 ∩ (𝐴 × 𝐴)) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ((𝑥 ∩ (𝐴 × 𝐴)) ∘ (𝑥 ∩ (𝐴 × 𝐴))) ⊆ (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
162140, 157, 161syl2anc 579 . . . . . . . . . 10 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) ∧ 𝑥𝑈) ∧ (𝑥𝑥) ⊆ 𝑢) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
163 ustexhalf 22293 . . . . . . . . . . 11 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → ∃𝑥𝑈 (𝑥𝑥) ⊆ 𝑢)
164163adantlr 706 . . . . . . . . . 10 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) → ∃𝑥𝑈 (𝑥𝑥) ⊆ 𝑢)
165162, 164r19.29a 3225 . . . . . . . . 9 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑢𝑈) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
166165ad4ant13 757 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴)))
167117sseq2d 3793 . . . . . . . . 9 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ((𝑤𝑤) ⊆ 𝑣 ↔ (𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
168167rexbidv 3199 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → (∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ (𝑢 ∩ (𝐴 × 𝐴))))
169166, 168mpbird 248 . . . . . . 7 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) ∧ 𝑢𝑈) ∧ 𝑣 = (𝑢 ∩ (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)
170169, 56r19.29a 3225 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)
171119, 135, 1703jca 1158 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣))
17260, 87, 1713jca 1158 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) ∧ 𝑣 ∈ (𝑈t (𝐴 × 𝐴))) → (∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))
173172ralrimiva 3113 . . 3 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))
1742, 20, 1733jca 1158 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣))))
175 isust 22286 . . 3 (𝐴 ∈ V → ((𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))))
17613, 175syl 17 . 2 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → ((𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴) ↔ ((𝑈t (𝐴 × 𝐴)) ⊆ 𝒫 (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∀𝑣 ∈ (𝑈t (𝐴 × 𝐴))(∀𝑤 ∈ 𝒫 (𝐴 × 𝐴)(𝑣𝑤𝑤 ∈ (𝑈t (𝐴 × 𝐴))) ∧ ∀𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑣𝑤) ∈ (𝑈t (𝐴 × 𝐴)) ∧ (( I ↾ 𝐴) ⊆ 𝑣𝑣 ∈ (𝑈t (𝐴 × 𝐴)) ∧ ∃𝑤 ∈ (𝑈t (𝐴 × 𝐴))(𝑤𝑤) ⊆ 𝑣)))))
177174, 176mpbird 248 1 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴𝑋) → (𝑈t (𝐴 × 𝐴)) ∈ (UnifOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  cun 3730  cin 3731  wss 3732  𝒫 cpw 4315   class class class wbr 4809   I cid 5184   × cxp 5275  ccnv 5276  dom cdm 5277  cres 5279  ccom 5281  cfv 6068  (class class class)co 6842  t crest 16349  UnifOncust 22282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-rest 16351  df-ust 22283
This theorem is referenced by:  restutop  22320  restutopopn  22321  ressust  22347  ressusp  22348  trcfilu  22377  cfiluweak  22378
  Copyright terms: Public domain W3C validator