This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 eqtrid ⊢ ( 𝐾 ∈ V → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )
30 4 29 syl ⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 < 𝑦 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) ) } )