Theorem ustn0

Description: The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017)

	Ref	Expression
Assertion	ustn0	⊢ ¬ ∅ ∈ ∪ ran UnifOn

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ ( 𝑥 × 𝑥 ) ∈ ∅
2		0ex	⊢ ∅ ∈ V
3		eleq2	⊢ ( 𝑢 = ∅ → ( ( 𝑥 × 𝑥 ) ∈ 𝑢 ↔ ( 𝑥 × 𝑥 ) ∈ ∅ ) )
4	2 3	elab	⊢ ( ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 } ↔ ( 𝑥 × 𝑥 ) ∈ ∅ )
5	1 4	mtbir	⊢ ¬ ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
6		vex	⊢ 𝑥 ∈ V
7		velpw	⊢ ( 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ↔ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
8	7	abbii	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
9		abid2	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = 𝒫 𝒫 ( 𝑥 × 𝑥 )
10	6 6	xpex	⊢ ( 𝑥 × 𝑥 ) ∈ V
11	10	pwex	⊢ 𝒫 ( 𝑥 × 𝑥 ) ∈ V
12	11	pwex	⊢ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ∈ V
13	9 12	eqeltri	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
14	8 13	eqeltrri	⊢ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
15		simp1	⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
16	15	ss2abi	⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
17	14 16	ssexi	⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V
18		df-ust	⊢ UnifOn = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
19	18	fvmpt2	⊢ ( ( 𝑥 ∈ V ∧ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V ) → ( UnifOn ‘ 𝑥 ) = { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
20	6 17 19	mp2an	⊢ ( UnifOn ‘ 𝑥 ) = { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) }
21		simp2	⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → ( 𝑥 × 𝑥 ) ∈ 𝑢 )
22	21	ss2abi	⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
23	20 22	eqsstri	⊢ ( UnifOn ‘ 𝑥 ) ⊆ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 }
24	23	sseli	⊢ ( ∅ ∈ ( UnifOn ‘ 𝑥 ) → ∅ ∈ { 𝑢 ∣ ( 𝑥 × 𝑥 ) ∈ 𝑢 } )
25	5 24	mto	⊢ ¬ ∅ ∈ ( UnifOn ‘ 𝑥 )
26	25	nex	⊢ ¬ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 )
27	18	funmpt2	⊢ Fun UnifOn
28		elunirn	⊢ ( Fun UnifOn → ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) ) )
29	27 28	ax-mp	⊢ ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) )
30		ustfn	⊢ UnifOn Fn V
31		fndm	⊢ ( UnifOn Fn V → dom UnifOn = V )
32	30 31	ax-mp	⊢ dom UnifOn = V
33	32	rexeqi	⊢ ( ∃ 𝑥 ∈ dom UnifOn ∅ ∈ ( UnifOn ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ V ∅ ∈ ( UnifOn ‘ 𝑥 ) )
34		rexv	⊢ ( ∃ 𝑥 ∈ V ∅ ∈ ( UnifOn ‘ 𝑥 ) ↔ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 ) )
35	29 33 34	3bitri	⊢ ( ∅ ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∅ ∈ ( UnifOn ‘ 𝑥 ) )
36	26 35	mtbir	⊢ ¬ ∅ ∈ ∪ ran UnifOn