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

Metamath Proof Explorer

Theorem diafn

Description: Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013)

Ref Expression
Hypotheses diafn.b ⊢ B = Base K
diafn.l ⊢ ≤ ˙ = ≤ K
diafn.h ⊢ H = LHyp ⁡ K
diafn.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diafn ⊢ K ∈ V ∧ W ∈ H → I Fn x ∈ B | x ≤ ˙ W

Proof

Step Hyp Ref Expression
1 diafn.b ⊢ B = Base K
2 diafn.l ⊢ ≤ ˙ = ≤ K
3 diafn.h ⊢ H = LHyp ⁡ K
4 diafn.i ⊢ I = DIsoA ⁡ K ⁡ W
5 fvex ⊢ LTrn ⁡ K ⁡ W ∈ V
6 5 rabex ⊢ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y ∈ V
7 eqid ⊢ y ∈ x ∈ B | x ≤ ˙ W ⟼ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y = y ∈ x ∈ B | x ≤ ˙ W ⟼ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y
8 6 7 fnmpti ⊢ y ∈ x ∈ B | x ≤ ˙ W ⟼ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y Fn x ∈ B | x ≤ ˙ W
9 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
10 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
11 1 2 3 9 10 4 diafval ⊢ K ∈ V ∧ W ∈ H → I = y ∈ x ∈ B | x ≤ ˙ W ⟼ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y
12 11 fneq1d ⊢ K ∈ V ∧ W ∈ H → I Fn x ∈ B | x ≤ ˙ W ↔ y ∈ x ∈ B | x ≤ ˙ W ⟼ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ y Fn x ∈ B | x ≤ ˙ W
13 8 12 mpbiri ⊢ K ∈ V ∧ W ∈ H → I Fn x ∈ B | x ≤ ˙ W