Metamath Proof Explorer


Theorem flval2

Description: An alternate way to define the floor function. (Contributed by NM, 16-Nov-2004)

Ref Expression
Assertion flval2 A A = ι x | x A y y A y x

Proof

Step Hyp Ref Expression
1 flle A A A
2 flge A y y A y A
3 2 biimpd A y y A y A
4 3 ralrimiva A y y A y A
5 flcl A A
6 zmax A ∃! x x A y y A y x
7 breq1 x = A x A A A
8 breq2 x = A y x y A
9 8 imbi2d x = A y A y x y A y A
10 9 ralbidv x = A y y A y x y y A y A
11 7 10 anbi12d x = A x A y y A y x A A y y A y A
12 11 riota2 A ∃! x x A y y A y x A A y y A y A ι x | x A y y A y x = A
13 5 6 12 syl2anc A A A y y A y A ι x | x A y y A y x = A
14 1 4 13 mpbi2and A ι x | x A y y A y x = A
15 14 eqcomd A A = ι x | x A y y A y x