Metamath Proof Explorer

Theorem dfttc4lem2

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

Ref Expression
Hypothesis dfttc4lem2.1 
|- B = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
Assertion dfttc4lem2 
|- ( A C_ B /\ Tr B )

Proof

Step Hyp Ref Expression
1 dfttc4lem2.1 
 |-  B = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
2 disjsn 
 |-  ( ( A i^i { u } ) = (/) <-> -. u e. A )
3 2 biimpi 
 |-  ( ( A i^i { u } ) = (/) -> -. u e. A )
4 3 necon2ai 
 |-  ( u e. A -> ( A i^i { u } ) =/= (/) )
5 elsni 
 |-  ( z e. { u } -> z = u )
6 5 a1d 
 |-  ( z e. { u } -> ( ( z i^i { u } ) = (/) -> z = u ) )
7 6 rgen 
 |-  A. z e. { u } ( ( z i^i { u } ) = (/) -> z = u )
8 vsnex 
 |-  { u } e. _V
9 vex 
 |-  u e. _V
10 1 8 9 dfttc4lem1 
 |-  ( ( ( A i^i { u } ) =/= (/) /\ A. z e. { u } ( ( z i^i { u } ) = (/) -> z = u ) ) -> u e. B )
11 4 7 10 sylancl 
 |-  ( u e. A -> u e. B )
12 11 ssriv 
 |-  A C_ B
13 vex 
 |-  v e. _V
14 simpr 
 |-  ( ( x = v /\ y = w ) -> y = w )
15 14 ineq2d 
 |-  ( ( x = v /\ y = w ) -> ( A i^i y ) = ( A i^i w ) )
16 15 neeq1d 
 |-  ( ( x = v /\ y = w ) -> ( ( A i^i y ) =/= (/) <-> ( A i^i w ) =/= (/) ) )
17 14 ineq2d 
 |-  ( ( x = v /\ y = w ) -> ( z i^i y ) = ( z i^i w ) )
18 17 eqeq1d 
 |-  ( ( x = v /\ y = w ) -> ( ( z i^i y ) = (/) <-> ( z i^i w ) = (/) ) )
19 simpl 
 |-  ( ( x = v /\ y = w ) -> x = v )
20 19 eqeq2d 
 |-  ( ( x = v /\ y = w ) -> ( z = x <-> z = v ) )
21 18 20 imbi12d 
 |-  ( ( x = v /\ y = w ) -> ( ( ( z i^i y ) = (/) -> z = x ) <-> ( ( z i^i w ) = (/) -> z = v ) ) )
22 14 21 raleqbidvv 
 |-  ( ( x = v /\ y = w ) -> ( A. z e. y ( ( z i^i y ) = (/) -> z = x ) <-> A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) )
23 16 22 anbi12d 
 |-  ( ( x = v /\ y = w ) -> ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) ) )
24 23 cbvexdvaw 
 |-  ( x = v -> ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> E. w ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) ) )
25 13 24 1 elab2 
 |-  ( v e. B <-> E. w ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) )
26 undisj2 
 |-  ( ( ( A i^i w ) = (/) /\ ( A i^i { u } ) = (/) ) <-> ( A i^i ( w u. { u } ) ) = (/) )
27 26 biimpri 
 |-  ( ( A i^i ( w u. { u } ) ) = (/) -> ( ( A i^i w ) = (/) /\ ( A i^i { u } ) = (/) ) )
28 27 simpld 
 |-  ( ( A i^i ( w u. { u } ) ) = (/) -> ( A i^i w ) = (/) )
29 28 necon3i 
 |-  ( ( A i^i w ) =/= (/) -> ( A i^i ( w u. { u } ) ) =/= (/) )
30 29 a1i 
 |-  ( u e. v -> ( ( A i^i w ) =/= (/) -> ( A i^i ( w u. { u } ) ) =/= (/) ) )
31 undisj2 
 |-  ( ( ( z i^i w ) = (/) /\ ( z i^i { u } ) = (/) ) <-> ( z i^i ( w u. { u } ) ) = (/) )
32 31 biimpri 
 |-  ( ( z i^i ( w u. { u } ) ) = (/) -> ( ( z i^i w ) = (/) /\ ( z i^i { u } ) = (/) ) )
33 32 simpld 
 |-  ( ( z i^i ( w u. { u } ) ) = (/) -> ( z i^i w ) = (/) )
34 33 imim1i 
 |-  ( ( ( z i^i w ) = (/) -> z = v ) -> ( ( z i^i ( w u. { u } ) ) = (/) -> z = v ) )
35 32 simprd 
 |-  ( ( z i^i ( w u. { u } ) ) = (/) -> ( z i^i { u } ) = (/) )
36 disjsn 
 |-  ( ( z i^i { u } ) = (/) <-> -. u e. z )
37 35 36 sylib 
 |-  ( ( z i^i ( w u. { u } ) ) = (/) -> -. u e. z )
38 elequ2 
 |-  ( z = v -> ( u e. z <-> u e. v ) )
39 38 biimprd 
 |-  ( z = v -> ( u e. v -> u e. z ) )
40 39 con3d 
 |-  ( z = v -> ( -. u e. z -> -. u e. v ) )
41 pm2.21 
 |-  ( -. u e. v -> ( u e. v -> z = u ) )
42 37 40 41 syl56 
 |-  ( z = v -> ( ( z i^i ( w u. { u } ) ) = (/) -> ( u e. v -> z = u ) ) )
43 34 42 syli 
 |-  ( ( ( z i^i w ) = (/) -> z = v ) -> ( ( z i^i ( w u. { u } ) ) = (/) -> ( u e. v -> z = u ) ) )
44 43 com3r 
 |-  ( u e. v -> ( ( ( z i^i w ) = (/) -> z = v ) -> ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) )
45 44 ralimdv 
 |-  ( u e. v -> ( A. z e. w ( ( z i^i w ) = (/) -> z = v ) -> A. z e. w ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) )
46 5 a1d 
 |-  ( z e. { u } -> ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) )
47 46 rgen 
 |-  A. z e. { u } ( ( z i^i ( w u. { u } ) ) = (/) -> z = u )
48 ralun 
 |-  ( ( A. z e. w ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) /\ A. z e. { u } ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) -> A. z e. ( w u. { u } ) ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) )
49 47 48 mpan2 
 |-  ( A. z e. w ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) -> A. z e. ( w u. { u } ) ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) )
50 45 49 syl6 
 |-  ( u e. v -> ( A. z e. w ( ( z i^i w ) = (/) -> z = v ) -> A. z e. ( w u. { u } ) ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) )
51 30 50 anim12d 
 |-  ( u e. v -> ( ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) -> ( ( A i^i ( w u. { u } ) ) =/= (/) /\ A. z e. ( w u. { u } ) ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) ) )
52 vex 
 |-  w e. _V
53 52 8 unex 
 |-  ( w u. { u } ) e. _V
54 1 53 9 dfttc4lem1 
 |-  ( ( ( A i^i ( w u. { u } ) ) =/= (/) /\ A. z e. ( w u. { u } ) ( ( z i^i ( w u. { u } ) ) = (/) -> z = u ) ) -> u e. B )
55 51 54 syl6 
 |-  ( u e. v -> ( ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) -> u e. B ) )
56 55 exlimdv 
 |-  ( u e. v -> ( E. w ( ( A i^i w ) =/= (/) /\ A. z e. w ( ( z i^i w ) = (/) -> z = v ) ) -> u e. B ) )
57 25 56 biimtrid 
 |-  ( u e. v -> ( v e. B -> u e. B ) )
58 57 imp 
 |-  ( ( u e. v /\ v e. B ) -> u e. B )
59 58 gen2 
 |-  A. u A. v ( ( u e. v /\ v e. B ) -> u e. B )
60 dftr2 
 |-  ( Tr B <-> A. u A. v ( ( u e. v /\ v e. B ) -> u e. B ) )
61 59 60 mpbir 
 |-  Tr B
62 12 61 pm3.2i 
 |-  ( A C_ B /\ Tr B )