cvrfval

Description: Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	cvrfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrfval.s	⊢ < = ( lt ‘ 𝐾 )
	cvrfval.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrfval	⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrfval.s	⊢ < = ( lt ‘ 𝐾 )
3		cvrfval.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		elex	⊢ ( 𝐾 ∈ 𝐴 → 𝐾 ∈ V )
5		fveq2	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
6	5 1	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
7	6	eleq2d	⊢ ( 𝑝 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑝 ) ↔ 𝑥 ∈ 𝐵 ) )
8	6	eleq2d	⊢ ( 𝑝 = 𝐾 → ( 𝑦 ∈ ( Base ‘ 𝑝 ) ↔ 𝑦 ∈ 𝐵 ) )
9	7 8	anbi12d	⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
10		fveq2	⊢ ( 𝑝 = 𝐾 → ( lt ‘ 𝑝 ) = ( lt ‘ 𝐾 ) )
11	10 2	eqtr4di	⊢ ( 𝑝 = 𝐾 → ( lt ‘ 𝑝 ) = < )
12	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( lt ‘ 𝑝 ) 𝑦 ↔ 𝑥 < 𝑦 ) )
13	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ↔ 𝑥 < 𝑧 ) )
14	11	breqd	⊢ ( 𝑝 = 𝐾 → ( 𝑧 ( lt ‘ 𝑝 ) 𝑦 ↔ 𝑧 < 𝑦 ) )
15	13 14	anbi12d	⊢ ( 𝑝 = 𝐾 → ( ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ↔ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) )
16	6 15	rexeqbidv	⊢ ( 𝑝 = 𝐾 → ( ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) )
17	16	notbid	⊢ ( 𝑝 = 𝐾 → ( ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ↔ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) )
18	9 12 17	3anbi123d	⊢ ( 𝑝 = 𝐾 → ( ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑥 ( lt ‘ 𝑝 ) 𝑦 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ) )
19	18	opabbidv	⊢ ( 𝑝 = 𝐾 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑥 ( lt ‘ 𝑝 ) 𝑦 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )
20		df-covers	⊢ ⋖ = ( 𝑝 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑥 ( lt ‘ 𝑝 ) 𝑦 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑥 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑦 ) ) } )
21		3anass	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ) )
22	21	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ) }
23	1	fvexi	⊢ 𝐵 ∈ V
24	23 23	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
25		opabssxp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ) } ⊆ ( 𝐵 × 𝐵 )
26	24 25	ssexi	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) ) } ∈ V
27	22 26	eqeltri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } ∈ V
28	19 20 27	fvmpt	⊢ ( 𝐾 ∈ V → ( ⋖ ‘ 𝐾 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )
29	3 28	syl5eq	⊢ ( 𝐾 ∈ V → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )
30	4 29	syl	⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )

Metamath Proof Explorer

Theorem cvrfval

Proof