Theorem lineset

Description: The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011)

	Ref	Expression
Hypotheses	lineset.l	⊢ ≤ = ( le ‘ 𝐾 )
	lineset.j	⊢ ∨ = ( join ‘ 𝐾 )
	lineset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	lineset.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
Assertion	lineset	⊢ ( 𝐾 ∈ 𝐵 → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )

Proof

Step	Hyp	Ref	Expression
1		lineset.l	⊢ ≤ = ( le ‘ 𝐾 )
2		lineset.j	⊢ ∨ = ( join ‘ 𝐾 )
3		lineset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		lineset.n	⊢ 𝑁 = ( Lines ‘ 𝐾 )
5		elex	⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
6		fveq2	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
7	6 3	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
8		fveq2	⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
9	8 1	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
10	9	breqd	⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ) )
11		fveq2	⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
12	11 2	eqtr4di	⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
13	12	oveqd	⊢ ( 𝑘 = 𝐾 → ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) = ( 𝑞 ∨ 𝑟 ) )
14	13	breq2d	⊢ ( 𝑘 = 𝐾 → ( 𝑝 ≤ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
15	10 14	bitrd	⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
16	7 15	rabeqbidv	⊢ ( 𝑘 = 𝐾 → { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
17	16	eqeq2d	⊢ ( 𝑘 = 𝐾 → ( 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ↔ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
18	17	anbi2d	⊢ ( 𝑘 = 𝐾 → ( ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
19	7 18	rexeqbidv	⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
20	7 19	rexeqbidv	⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
21	20	abbidv	⊢ ( 𝑘 = 𝐾 → { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
22		df-lines	⊢ Lines = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )
23	3	fvexi	⊢ 𝐴 ∈ V
24		df-sn	⊢ { { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } = { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } }
25		snex	⊢ { { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } ∈ V
26	24 25	eqeltrri	⊢ { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } ∈ V
27		simpr	⊢ ( ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
28	27	ss2abi	⊢ { 𝑠 ∣ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ⊆ { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } }
29	26 28	ssexi	⊢ { 𝑠 ∣ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ∈ V
30	23 23 29	ab2rexex2	⊢ { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ∈ V
31	21 22 30	fvmpt	⊢ ( 𝐾 ∈ V → ( Lines ‘ 𝐾 ) = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
32	4 31	syl5eq	⊢ ( 𝐾 ∈ V → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
33	5 32	syl	⊢ ( 𝐾 ∈ 𝐵 → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )