Metamath Proof Explorer

Definition df-disoa

Description: Define partial isomorphism A. (Contributed by NM, 15-Oct-2013)

Ref Expression
Assertion df-disoa ⊢ DIsoA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdia class DIsoA
1 vk setvar k
2 cvv class V
3 vw setvar w
4 clh class LHyp
5 1 cv setvar k
6 5 4 cfv class LHyp ⁡ k
7 vx setvar x
8 vy setvar y
9 cbs class Base
10 5 9 cfv class Base k
11 8 cv setvar y
12 cple class le
13 5 12 cfv class ≤ k
14 3 cv setvar w
15 11 14 13 wbr wff y ≤ k w
16 15 8 10 crab class y ∈ Base k | y ≤ k w
17 vf setvar f
18 cltrn class LTrn
19 5 18 cfv class LTrn ⁡ k
20 14 19 cfv class LTrn ⁡ k ⁡ w
21 ctrl class trL
22 5 21 cfv class trL ⁡ k
23 14 22 cfv class trL ⁡ k ⁡ w
24 17 cv setvar f
25 24 23 cfv class trL ⁡ k ⁡ w ⁡ f
26 7 cv setvar x
27 25 26 13 wbr wff trL ⁡ k ⁡ w ⁡ f ≤ k x
28 27 17 20 crab class f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x
29 7 16 28 cmpt class x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x
30 3 6 29 cmpt class w ∈ LHyp ⁡ k ⟼ x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x
31 1 2 30 cmpt class k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x
32 0 31 wceq wff DIsoA = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ y ∈ Base k | y ≤ k w ⟼ f ∈ LTrn ⁡ k ⁡ w | trL ⁡ k ⁡ w ⁡ f ≤ k x