Metamath Proof Explorer

Theorem dfttc4lem1

Description: Lemma for dfttc4 . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Hypotheses dfttc4lem1.1 
|- B = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
dfttc4lem1.2 
|- C e. _V
dfttc4lem1.3 
|- D e. _V
Assertion dfttc4lem1 
|- ( ( ( A i^i C ) =/= (/) /\ A. z e. C ( ( z i^i C ) = (/) -> z = D ) ) -> D e. B )

Proof

Step Hyp Ref Expression
1 dfttc4lem1.1 
 |-  B = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
2 dfttc4lem1.2 
 |-  C e. _V
3 dfttc4lem1.3 
 |-  D e. _V
4 ineq2 
 |-  ( y = C -> ( A i^i y ) = ( A i^i C ) )
5 4 neeq1d 
 |-  ( y = C -> ( ( A i^i y ) =/= (/) <-> ( A i^i C ) =/= (/) ) )
6 ineq2 
 |-  ( y = C -> ( z i^i y ) = ( z i^i C ) )
7 6 eqeq1d 
 |-  ( y = C -> ( ( z i^i y ) = (/) <-> ( z i^i C ) = (/) ) )
8 7 imbi1d 
 |-  ( y = C -> ( ( ( z i^i y ) = (/) -> z = D ) <-> ( ( z i^i C ) = (/) -> z = D ) ) )
9 8 raleqbi1dv 
 |-  ( y = C -> ( A. z e. y ( ( z i^i y ) = (/) -> z = D ) <-> A. z e. C ( ( z i^i C ) = (/) -> z = D ) ) )
10 5 9 anbi12d 
 |-  ( y = C -> ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) <-> ( ( A i^i C ) =/= (/) /\ A. z e. C ( ( z i^i C ) = (/) -> z = D ) ) ) )
11 2 10 spcev 
 |-  ( ( ( A i^i C ) =/= (/) /\ A. z e. C ( ( z i^i C ) = (/) -> z = D ) ) -> E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) )
12 eqeq2 
 |-  ( x = D -> ( z = x <-> z = D ) )
13 12 imbi2d 
 |-  ( x = D -> ( ( ( z i^i y ) = (/) -> z = x ) <-> ( ( z i^i y ) = (/) -> z = D ) ) )
14 13 ralbidv 
 |-  ( x = D -> ( A. z e. y ( ( z i^i y ) = (/) -> z = x ) <-> A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) )
15 14 anbi2d 
 |-  ( x = D -> ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) ) )
16 15 exbidv 
 |-  ( x = D -> ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) ) )
17 3 16 1 elab2 
 |-  ( D e. B <-> E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = D ) ) )
18 11 17 sylibr 
 |-  ( ( ( A i^i C ) =/= (/) /\ A. z e. C ( ( z i^i C ) = (/) -> z = D ) ) -> D e. B )