Metamath Proof Explorer

Theorem dicvalrelN

Description: The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicvalrel.h ⊢ H = LHyp ⁡ K
dicvalrel.i ⊢ I = DIsoC ⁡ K ⁡ W
Assertion dicvalrelN ⊢ K ∈ V ∧ W ∈ H → Rel ⁡ I ⁡ X

Proof

Step Hyp Ref Expression
1 dicvalrel.h ⊢ H = LHyp ⁡ K
2 dicvalrel.i ⊢ I = DIsoC ⁡ K ⁡ W
3 relopabv ⊢ Rel ⁡ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = X ∧ s ∈ TEndo ⁡ K ⁡ W
4 eqid ⊢ ≤ K = ≤ K
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 4 5 1 2 dicdmN ⊢ K ∈ V ∧ W ∈ H → dom ⁡ I = p ∈ Atoms ⁡ K | ¬ p ≤ K W
7 6 eleq2d ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ p ∈ Atoms ⁡ K | ¬ p ≤ K W
8 breq1 ⊢ p = X → p ≤ K W ↔ X ≤ K W
9 8 notbid ⊢ p = X → ¬ p ≤ K W ↔ ¬ X ≤ K W
10 9 elrab ⊢ X ∈ p ∈ Atoms ⁡ K | ¬ p ≤ K W ↔ X ∈ Atoms ⁡ K ∧ ¬ X ≤ K W
11 7 10 bitrdi ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I ↔ X ∈ Atoms ⁡ K ∧ ¬ X ≤ K W
12 11 biimpa ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → X ∈ Atoms ⁡ K ∧ ¬ X ≤ K W
13 eqid ⊢ oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
14 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
15 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
16 4 5 1 13 14 15 2 dicval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ Atoms ⁡ K ∧ ¬ X ≤ K W → I ⁡ X = f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = X ∧ s ∈ TEndo ⁡ K ⁡ W
17 12 16 syldan ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → I ⁡ X = f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = X ∧ s ∈ TEndo ⁡ K ⁡ W
18 17 releqd ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → Rel ⁡ I ⁡ X ↔ Rel ⁡ f s | f = s ⁡ ι g ∈ LTrn ⁡ K ⁡ W | g ⁡ oc ⁡ K ⁡ W = X ∧ s ∈ TEndo ⁡ K ⁡ W
19 3 18 mpbiri ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ dom ⁡ I → Rel ⁡ I ⁡ X
20 19 ex ⊢ K ∈ V ∧ W ∈ H → X ∈ dom ⁡ I → Rel ⁡ I ⁡ X
21 rel0 ⊢ Rel ⁡ ∅
22 ndmfv ⊢ ¬ X ∈ dom ⁡ I → I ⁡ X = ∅
23 22 releqd ⊢ ¬ X ∈ dom ⁡ I → Rel ⁡ I ⁡ X ↔ Rel ⁡ ∅
24 21 23 mpbiri ⊢ ¬ X ∈ dom ⁡ I → Rel ⁡ I ⁡ X
25 20 24 pm2.61d1 ⊢ K ∈ V ∧ W ∈ H → Rel ⁡ I ⁡ X