Theorem dicval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	dicval.l	⊢ ≤ = ( le ‘ 𝐾 )
	dicval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dicval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dicval.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
	dicval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dicval.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dicval.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
Assertion	dicval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )

Proof

Step	Hyp	Ref	Expression
1		dicval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dicval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		dicval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		dicval.p	⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
5		dicval.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		dicval.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
7		dicval.i	⊢ 𝐼 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
8	1 2 3 4 5 6 7	dicfval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) )
9	8	adantr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐼 = ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) )
10	9	fveq1d	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = ( ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) ‘ 𝑄 ) )
11		simpr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
12		breq1	⊢ ( 𝑟 = 𝑄 → ( 𝑟 ≤ 𝑊 ↔ 𝑄 ≤ 𝑊 ) )
13	12	notbid	⊢ ( 𝑟 = 𝑄 → ( ¬ 𝑟 ≤ 𝑊 ↔ ¬ 𝑄 ≤ 𝑊 ) )
14	13	elrab	⊢ ( 𝑄 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↔ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
15	11 14	sylibr	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝑄 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } )
16		eqeq2	⊢ ( 𝑞 = 𝑄 → ( ( 𝑔 ‘ 𝑃 ) = 𝑞 ↔ ( 𝑔 ‘ 𝑃 ) = 𝑄 ) )
17	16	riotabidv	⊢ ( 𝑞 = 𝑄 → ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) )
18	17	fveq2d	⊢ ( 𝑞 = 𝑄 → ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )
19	18	eqeq2d	⊢ ( 𝑞 = 𝑄 → ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ↔ 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ) )
20	19	anbi1d	⊢ ( 𝑞 = 𝑄 → ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) ↔ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) ) )
21	20	opabbidv	⊢ ( 𝑞 = 𝑄 → { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
22		eqid	⊢ ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) = ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
23	6	fvexi	⊢ 𝐸 ∈ V
24	23	uniex	⊢ ∪ 𝐸 ∈ V
25	24	rnex	⊢ ran ∪ 𝐸 ∈ V
26	25	uniex	⊢ ∪ ran ∪ 𝐸 ∈ V
27	26	pwex	⊢ 𝒫 ∪ ran ∪ 𝐸 ∈ V
28	27 23	xpex	⊢ ( 𝒫 ∪ ran ∪ 𝐸 × 𝐸 ) ∈ V
29		simpl	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) )
30		fvssunirn	⊢ ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ⊆ ∪ ran 𝑠
31		elssuni	⊢ ( 𝑠 ∈ 𝐸 → 𝑠 ⊆ ∪ 𝐸 )
32	31	adantl	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → 𝑠 ⊆ ∪ 𝐸 )
33		rnss	⊢ ( 𝑠 ⊆ ∪ 𝐸 → ran 𝑠 ⊆ ran ∪ 𝐸 )
34		uniss	⊢ ( ran 𝑠 ⊆ ran ∪ 𝐸 → ∪ ran 𝑠 ⊆ ∪ ran ∪ 𝐸 )
35	32 33 34	3syl	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → ∪ ran 𝑠 ⊆ ∪ ran ∪ 𝐸 )
36	30 35	sstrid	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ⊆ ∪ ran ∪ 𝐸 )
37	26	elpw2	⊢ ( ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∈ 𝒫 ∪ ran ∪ 𝐸 ↔ ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ⊆ ∪ ran ∪ 𝐸 )
38	36 37	sylibr	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∈ 𝒫 ∪ ran ∪ 𝐸 )
39	29 38	eqeltrd	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 )
40		simpr	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → 𝑠 ∈ 𝐸 )
41	39 40	jca	⊢ ( ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) → ( 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸 ) )
42	41	ssopab2i	⊢ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } ⊆ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸 ) }
43		df-xp	⊢ ( 𝒫 ∪ ran ∪ 𝐸 × 𝐸 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 ∈ 𝒫 ∪ ran ∪ 𝐸 ∧ 𝑠 ∈ 𝐸 ) }
44	42 43	sseqtrri	⊢ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } ⊆ ( 𝒫 ∪ ran ∪ 𝐸 × 𝐸 )
45	28 44	ssexi	⊢ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } ∈ V
46	21 22 45	fvmpt	⊢ ( 𝑄 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } → ( ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
47	15 46	syl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑞 ∈ { 𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊 } ↦ { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑞 ) ) ∧ 𝑠 ∈ 𝐸 ) } ) ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )
48	10 47	eqtrd	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑄 ) = { ⟨ 𝑓 , 𝑠 ⟩ ∣ ( 𝑓 = ( 𝑠 ‘ ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 ) ) ∧ 𝑠 ∈ 𝐸 ) } )