Theorem isust 24528

Description: The predicate "𝑈 is a uniform structure with base 𝑋". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)

Assertion

Ref	Expression
isust	⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))

Distinct variable groups:   𝑤,𝑣,𝑈   𝑣,𝑋,𝑤

Allowed substitution hints:   𝑉(𝑤, 𝑣)

Proof of Theorem isust

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ustval 24527	. . 3 ⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
2	1	eleq2d 2846	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ 𝑈 ∈ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))}))
3		simp1 1154	. . . 4 ⊢ ((𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))) → 𝑈 ⊆ 𝒫 (𝑋 × 𝑋))
4		sqxpexg 7769	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → (𝑋 × 𝑋) ∈ V)
5	4	pwexd 5340	. . . . . . 7 ⊢ (𝑋 ∈ 𝑉 → 𝒫 (𝑋 × 𝑋) ∈ V)
6	5	adantr 486	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 (𝑋 × 𝑋)) → 𝒫 (𝑋 × 𝑋) ∈ V)
7		simpr 490	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 (𝑋 × 𝑋)) → 𝑈 ⊆ 𝒫 (𝑋 × 𝑋))
8	6, 7	ssexd 5285	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 (𝑋 × 𝑋)) → 𝑈 ∈ V)
9	8	ex 418	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) → 𝑈 ∈ V))
10	3, 9	syl5 35	. . 3 ⊢ (𝑋 ∈ 𝑉 → ((𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))) → 𝑈 ∈ V))
11		sseq1 3933	. . . . 5 ⊢ (𝑢 = 𝑈 → (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ↔ 𝑈 ⊆ 𝒫 (𝑋 × 𝑋)))
12		eleq2 2849	. . . . 5 ⊢ (𝑢 = 𝑈 → ((𝑋 × 𝑋) ∈ 𝑢 ↔ (𝑋 × 𝑋) ∈ 𝑈))
13		eleq2 2849	. . . . . . . . 9 ⊢ (𝑢 = 𝑈 → (𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑈))
14	13	imbi2d 343	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ↔ (𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈)))
15	14	ralbidv 3185	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈)))
16		eleq2 2849	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → ((𝑣 ∩ 𝑤) ∈ 𝑢 ↔ (𝑣 ∩ 𝑤) ∈ 𝑈))
17	16	raleqbi1dv 3329	. . . . . . 7 ⊢ (𝑢 = 𝑈 → (∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ↔ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈))
18		eleq2 2849	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (◡𝑣 ∈ 𝑢 ↔ ◡𝑣 ∈ 𝑈))
19		rexeq 3315	. . . . . . . 8 ⊢ (𝑢 = 𝑈 → (∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))
20	18, 19	3anbi23d 1467	. . . . . . 7 ⊢ (𝑢 = 𝑈 → ((( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣) ↔ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))
21	15, 17, 20	3anbi123d 1464	. . . . . 6 ⊢ (𝑢 = 𝑈 → ((∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))))
22	21	raleqbi1dv 3329	. . . . 5 ⊢ (𝑢 = 𝑈 → (∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))))
23	11, 12, 22	3anbi123d 1464	. . . 4 ⊢ (𝑢 = 𝑈 → ((𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
24	23	elab3g 3638	. . 3 ⊢ (((𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣))) → 𝑈 ∈ V) → (𝑈 ∈ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
25	10, 24	syl 18	. 2 ⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
26	2, 25	bitrd 282	1 ⊢ (𝑋 ∈ 𝑉 → (𝑈 ∈ (UnifOn‘𝑋) ↔ (𝑈 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑈 ∧ ∀𝑣 ∈ 𝑈 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈) ∧ ∀𝑤 ∈ 𝑈 (𝑣 ∩ 𝑤) ∈ 𝑈 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑈 ∧ ∃𝑤 ∈ 𝑈 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  {cab 2738  ∀wral 3076  ∃wrex 3086  Vcvv 3450   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556   I cid 5544   × cxp 5648  ^◡ccnv 5649   ↾ cres 5652   ∘ ccom 5654  ‘cfv 6538  UnifOncust 24524

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-res 5662  df-iota 6494  df-fun 6540  df-fv 6546  df-ust 24525

This theorem is used by:  ustssxp  24529  ustssel  24530  ustbasel  24531  ustincl  24532  ustdiag  24533  ustinvel  24534  ustexhalf  24535  ustfilxp  24537  ust0  24544  ustbas2  24549  trust  24553  metust  24882