Metamath Proof Explorer

Theorem dfac5prim

Description: dfac5 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion dfac5prim 
|- ( CHOICE <-> A. x ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac5 
 |-  ( CHOICE <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
2 n0 
 |-  ( z =/= (/) <-> E. w w e. z )
3 2 ralbii 
 |-  ( A. z e. x z =/= (/) <-> A. z e. x E. w w e. z )
4 df-ral 
 |-  ( A. z e. x E. w w e. z <-> A. z ( z e. x -> E. w w e. z ) )
5 3 4 bitri 
 |-  ( A. z e. x z =/= (/) <-> A. z ( z e. x -> E. w w e. z ) )
6 df-ne 
 |-  ( z =/= w <-> -. z = w )
7 disj1 
 |-  ( ( z i^i w ) = (/) <-> A. y ( y e. z -> -. y e. w ) )
8 6 7 imbi12i 
 |-  ( ( z =/= w -> ( z i^i w ) = (/) ) <-> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) )
9 8 2ralbii 
 |-  ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. x A. w e. x ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) )
10 r2al 
 |-  ( A. z e. x A. w e. x ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) <-> A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) )
11 9 10 bitri 
 |-  ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) )
12 5 11 anbi12i 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) <-> ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) )
13 elin 
 |-  ( v e. ( z i^i y ) <-> ( v e. z /\ v e. y ) )
14 13 eubii 
 |-  ( E! v v e. ( z i^i y ) <-> E! v ( v e. z /\ v e. y ) )
15 eu6 
 |-  ( E! v ( v e. z /\ v e. y ) <-> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) )
16 14 15 bitri 
 |-  ( E! v v e. ( z i^i y ) <-> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) )
17 16 ralbii 
 |-  ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) )
18 df-ral 
 |-  ( A. z e. x E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) <-> A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )
19 17 18 bitri 
 |-  ( A. z e. x E! v v e. ( z i^i y ) <-> A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )
20 19 exbii 
 |-  ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) )
21 12 20 imbi12i 
 |-  ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
22 21 albii 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )
23 1 22 bitri 
 |-  ( CHOICE <-> A. x ( ( A. z ( z e. x -> E. w w e. z ) /\ A. z A. w ( ( z e. x /\ w e. x ) -> ( -. z = w -> A. y ( y e. z -> -. y e. w ) ) ) ) -> E. y A. z ( z e. x -> E. w A. v ( ( v e. z /\ v e. y ) <-> v = w ) ) ) )