df-disoa

		Ref	Expression
	Assertion	df-disoa	$⊢ DIsoA = (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in \{y \in {Base}_{k} \| y \leq_{k} w\} ⟼ \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\})))$

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 \leq_{k}$
14	3	cv	$setvar w$
15	11 14 13	wbr	$wff y \leq_{k} w$
16	15 8 10	crab	$class \{y \in {Base}_{k} \| y \leq_{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) \leq_{k} x$
28	27 17 20	crab	$class \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\}$
29	7 16 28	cmpt	$class (x \in \{y \in {Base}_{k} \| y \leq_{k} w\} ⟼ \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\})$
30	3 6 29	cmpt	$class (w \in LHyp (k) ⟼ (x \in \{y \in {Base}_{k} \| y \leq_{k} w\} ⟼ \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\}))$
31	1 2 30	cmpt	$class (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in \{y \in {Base}_{k} \| y \leq_{k} w\} ⟼ \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\})))$
32	0 31	wceq	$wff DIsoA = (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in \{y \in {Base}_{k} \| y \leq_{k} w\} ⟼ \{f \in LTrn (k) (w) \| trL (k) (w) (f) \leq_{k} x\})))$

Metamath Proof Explorer