Theorem meetval

Description: Meet value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom G requirement. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	meetdef.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
	meetdef.m	⊢ ∧ = ( meet ‘ 𝐾 )
	meetdef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	meetdef.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
	meetdef.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
Assertion	meetval	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		meetdef.u	⊢ 𝐺 = ( glb ‘ 𝐾 )
2		meetdef.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		meetdef.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		meetdef.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
5		meetdef.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑍 )
6	1 2	meetfval2	⊢ ( 𝐾 ∈ 𝑉 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )
7	3 6	syl	⊢ ( 𝜑 → ∧ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } )
8	7	oveqd	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) )
9	8	adantr	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) )
10		simpr	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → { 𝑋 , 𝑌 } ∈ dom 𝐺 )
11		eqidd	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
12		fvexd	⊢ ( 𝜑 → ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ∈ V )
13		preq12	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → { 𝑥 , 𝑦 } = { 𝑋 , 𝑌 } )
14	13	eleq1d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) )
15	14	3adant3	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) )
16		simp3	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
17	13	fveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
18	17	3adant3	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝐺 ‘ { 𝑥 , 𝑦 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
19	16 18	eqeq12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ↔ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) )
20	15 19	anbi12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ∧ 𝑧 = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( { 𝑋 , 𝑌 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) ) )
21		moeq	⊢ ∃* 𝑧 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } )
22	21	moani	⊢ ∃* 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) )
23		eqid	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) }
24	20 22 23	ovigg	⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑍 ∧ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ∈ V ) → ( ( { 𝑋 , 𝑌 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) )
25	4 5 12 24	syl3anc	⊢ ( 𝜑 → ( ( { 𝑋 , 𝑌 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( ( { 𝑋 , 𝑌 } ∈ dom 𝐺 ∧ ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) ) )
27	10 11 26	mp2and	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝑋 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝐺 ∧ 𝑧 = ( 𝐺 ‘ { 𝑥 , 𝑦 } ) ) } 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
28	9 27	eqtrd	⊢ ( ( 𝜑 ∧ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
29	1 2 3 4 5	meetdef	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ↔ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) )
30	29	notbid	⊢ ( 𝜑 → ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ↔ ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) )
31		df-ov	⊢ ( 𝑋 ∧ 𝑌 ) = ( ∧ ‘ ⟨ 𝑋 , 𝑌 ⟩ )
32		ndmfv	⊢ ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ → ( ∧ ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ∅ )
33	31 32	eqtrid	⊢ ( ¬ ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ → ( 𝑋 ∧ 𝑌 ) = ∅ )
34	30 33	biimtrrdi	⊢ ( 𝜑 → ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 → ( 𝑋 ∧ 𝑌 ) = ∅ ) )
35	34	imp	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝑋 ∧ 𝑌 ) = ∅ )
36		ndmfv	⊢ ( ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 → ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ∅ )
37	36	adantl	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝐺 ‘ { 𝑋 , 𝑌 } ) = ∅ )
38	35 37	eqtr4d	⊢ ( ( 𝜑 ∧ ¬ { 𝑋 , 𝑌 } ∈ dom 𝐺 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )
39	28 38	pm2.61dan	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) = ( 𝐺 ‘ { 𝑋 , 𝑌 } ) )