Theorem ustval 24243

Description: The class of all uniform structures for a base 𝑋. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)

Assertion

Ref	Expression
ustval	⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})

Distinct variable group:   𝑣,𝑢,𝑤,𝑋

Allowed substitution hints:   𝑉(𝑤,𝑣,𝑢)

Proof of Theorem ustval

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ust 24241	. 2 ⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
2		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
3	2	sqxpeqd 5677	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 × 𝑥) = (𝑋 × 𝑋))
4	3	pweqd 4571	. . . . 5 ⊢ (𝑥 = 𝑋 → 𝒫 (𝑥 × 𝑥) = 𝒫 (𝑋 × 𝑋))
5	4	sseq2d 3968	. . . 4 ⊢ (𝑥 = 𝑋 → (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ↔ 𝑢 ⊆ 𝒫 (𝑋 × 𝑋)))
6	3	eleq1d 2846	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝑥 × 𝑥) ∈ 𝑢 ↔ (𝑋 × 𝑋) ∈ 𝑢))
7	4	raleqdv 3319	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ↔ ∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢)))
8		reseq2 5958	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ( I ↾ 𝑥) = ( I ↾ 𝑋))
9	8	sseq1d 3967	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (( I ↾ 𝑥) ⊆ 𝑣 ↔ ( I ↾ 𝑋) ⊆ 𝑣))
10	9	3anbi1d 1460	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣) ↔ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))
11	7, 10	3anbi13d 1458	. . . . 5 ⊢ (𝑥 = 𝑋 → ((∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))))
12	11	ralbidv 3184	. . . 4 ⊢ (𝑥 = 𝑋 → (∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))))
13	5, 6, 12	3anbi123d 1456	. . 3 ⊢ (𝑥 = 𝑋 → ((𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))) ↔ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))))
14	13	abbidv 2827	. 2 ⊢ (𝑥 = 𝑋 → {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
15		elex 3474	. 2 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ V)
16		simp1 1148	. . . . 5 ⊢ ((𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))) → 𝑢 ⊆ 𝒫 (𝑋 × 𝑋))
17	16	ss2abi 4019	. . . 4 ⊢ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ⊆ {𝑢 ∣ 𝑢 ⊆ 𝒫 (𝑋 × 𝑋)}
18		df-pw 4556	. . . 4 ⊢ 𝒫 𝒫 (𝑋 × 𝑋) = {𝑢 ∣ 𝑢 ⊆ 𝒫 (𝑋 × 𝑋)}
19	17, 18	sseqtrri 3985	. . 3 ⊢ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ⊆ 𝒫 𝒫 (𝑋 × 𝑋)
20		sqxpexg 7734	. . . 4 ⊢ (𝑋 ∈ 𝑉 → (𝑋 × 𝑋) ∈ V)
21		pwexg 5334	. . . 4 ⊢ ((𝑋 × 𝑋) ∈ V → 𝒫 (𝑋 × 𝑋) ∈ V)
22		pwexg 5334	. . . 4 ⊢ (𝒫 (𝑋 × 𝑋) ∈ V → 𝒫 𝒫 (𝑋 × 𝑋) ∈ V)
23	20, 21, 22	3syl 18	. . 3 ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝒫 (𝑋 × 𝑋) ∈ V)
24		ssexg 5278	. . 3 ⊢ (({𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ⊆ 𝒫 𝒫 (𝑋 × 𝑋) ∧ 𝒫 𝒫 (𝑋 × 𝑋) ∈ V) → {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ∈ V)
25	19, 23, 24	sylancr 596	. 2 ⊢ (𝑋 ∈ 𝑉 → {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))} ∈ V)
26	1, 14, 15, 25	fvmptd3 6995	1 ⊢ (𝑋 ∈ 𝑉 → (UnifOn‘𝑋) = {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑋 × 𝑋)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑋) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})

Syntax hints:   → wi 4   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  ∃wrex 3085  Vcvv 3453   ∩ cin 3903   ⊆ wss 3904  𝒫 cpw 4554   I cid 5539   × cxp 5643  ^◡ccnv 5644   ↾ cres 5647   ∘ ccom 5649  ‘cfv 6517  UnifOncust 24240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-res 5657  df-iota 6473  df-fun 6519  df-fv 6525  df-ust 24241

This theorem is referenced by:  isust  24244