Theorem meet0

Description: Lemma for odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015) TODO ( df-riota update): This proof increased from 152 bytes to 547 bytes after the df-riota change. Any way to shorten it? join0 also.

	Ref	Expression
Assertion	meet0	⊢ ( meet ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		eqid	⊢ ( glb ‘ ∅ ) = ( glb ‘ ∅ )
3		eqid	⊢ ( meet ‘ ∅ ) = ( meet ‘ ∅ )
4	2 3	meetfval	⊢ ( ∅ ∈ V → ( meet ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } )
5	1 4	ax-mp	⊢ ( meet ‘ ∅ ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 }
6		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ) }
7		br0	⊢ ¬ { 𝑥 , 𝑦 } ∅ 𝑧
8		base0	⊢ ∅ = ( Base ‘ ∅ )
9		eqid	⊢ ( le ‘ ∅ ) = ( le ‘ ∅ )
10		biid	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) )
11		id	⊢ ( ∅ ∈ V → ∅ ∈ V )
12	8 9 2 10 11	glbfval	⊢ ( ∅ ∈ V → ( glb ‘ ∅ ) = ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } ) )
13	1 12	ax-mp	⊢ ( glb ‘ ∅ ) = ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } )
14		reu0	⊢ ¬ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) )
15	14	abf	⊢ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } = ∅
16	15	reseq2i	⊢ ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } ) = ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ ∅ )
17		res0	⊢ ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ ∅ ) = ∅
18	16 17	eqtri	⊢ ( ( 𝑥 ∈ 𝒫 ∅ ↦ ( ℩ 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) ) ) ↾ { 𝑥 ∣ ∃! 𝑦 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑦 ( le ‘ ∅ ) 𝑧 ∧ ∀ 𝑤 ∈ ∅ ( ∀ 𝑧 ∈ 𝑥 𝑤 ( le ‘ ∅ ) 𝑧 → 𝑤 ( le ‘ ∅ ) 𝑦 ) ) } ) = ∅
19	13 18	eqtri	⊢ ( glb ‘ ∅ ) = ∅
20	19	breqi	⊢ ( { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ↔ { 𝑥 , 𝑦 } ∅ 𝑧 )
21	7 20	mtbir	⊢ ¬ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧
22	21	intnan	⊢ ¬ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
23	22	nex	⊢ ¬ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
24	23	nex	⊢ ¬ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
25	24	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 )
26	25	abf	⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 ) } = ∅
27	6 26	eqtri	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( glb ‘ ∅ ) 𝑧 } = ∅
28	5 27	eqtri	⊢ ( meet ‘ ∅ ) = ∅