Metamath Proof Explorer

Theorem kardenOLD

Description: Obsolete version of karden as of 19-Jul-2026. (Contributed by NM, 18-Dec-2003) (Revised by AV, 12-Jul-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses kardenOLD.a 
|- A e. _V
kardenOLD.c 
|- C = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) }
kardenOLD.d 
|- D = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) }
Assertion kardenOLD 
|- ( C = D <-> A ~~ B )

Proof

Step Hyp Ref Expression
1 kardenOLD.a 
 |-  A e. _V
2 kardenOLD.c 
 |-  C = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) }
3 kardenOLD.d 
 |-  D = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) }
4 breq1 
 |-  ( w = A -> ( w ~~ A <-> A ~~ A ) )
5 1 enref 
 |-  A ~~ A
6 1 4 5 ceqsexv2d 
 |-  E. w w ~~ A
7 abn0 
 |-  ( { w | w ~~ A } =/= (/) <-> E. w w ~~ A )
8 6 7 mpbir 
 |-  { w | w ~~ A } =/= (/)
9 scott0OLD 
 |-  ( { w | w ~~ A } = (/) <-> { z e. { w | w ~~ A } | A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) } = (/) )
10 9 necon3bii 
 |-  ( { w | w ~~ A } =/= (/) <-> { z e. { w | w ~~ A } | A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) } =/= (/) )
11 8 10 mpbi 
 |-  { z e. { w | w ~~ A } | A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) } =/= (/)
12 rabn0 
 |-  ( { z e. { w | w ~~ A } | A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) } =/= (/) <-> E. z e. { w | w ~~ A } A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) )
13 11 12 mpbi 
 |-  E. z e. { w | w ~~ A } A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y )
14 vex 
 |-  z e. _V
15 breq1 
 |-  ( w = z -> ( w ~~ A <-> z ~~ A ) )
16 14 15 elab 
 |-  ( z e. { w | w ~~ A } <-> z ~~ A )
17 breq1 
 |-  ( w = y -> ( w ~~ A <-> y ~~ A ) )
18 17 ralab 
 |-  ( A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) <-> A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) )
19 16 18 anbi12i 
 |-  ( ( z e. { w | w ~~ A } /\ A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) ) <-> ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) )
20 simpl 
 |-  ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) -> z ~~ A )
21 20 a1i 
 |-  ( C = D -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) -> z ~~ A ) )
22 2 3 eqeq12i 
 |-  ( C = D <-> { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } )
23 abbib 
 |-  ( { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } <-> A. x ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) ) )
24 22 23 bitri 
 |-  ( C = D <-> A. x ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) ) )
25 breq1 
 |-  ( x = z -> ( x ~~ A <-> z ~~ A ) )
26 fveq2 
 |-  ( x = z -> ( rank ` x ) = ( rank ` z ) )
27 26 sseq1d 
 |-  ( x = z -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` z ) C_ ( rank ` y ) ) )
28 27 imbi2d 
 |-  ( x = z -> ( ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) )
29 28 albidv 
 |-  ( x = z -> ( A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) )
30 25 29 anbi12d 
 |-  ( x = z -> ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) ) )
31 breq1 
 |-  ( x = z -> ( x ~~ B <-> z ~~ B ) )
32 27 imbi2d 
 |-  ( x = z -> ( ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) )
33 32 albidv 
 |-  ( x = z -> ( A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) )
34 31 33 anbi12d 
 |-  ( x = z -> ( ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( z ~~ B /\ A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) ) )
35 30 34 bibi12d 
 |-  ( x = z -> ( ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) ) <-> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) <-> ( z ~~ B /\ A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) ) ) )
36 35 spvv 
 |-  ( A. x ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) ) -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) <-> ( z ~~ B /\ A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) ) )
37 24 36 sylbi 
 |-  ( C = D -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) <-> ( z ~~ B /\ A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) ) )
38 simpl 
 |-  ( ( z ~~ B /\ A. y ( y ~~ B -> ( rank ` z ) C_ ( rank ` y ) ) ) -> z ~~ B )
39 37 38 biimtrdi 
 |-  ( C = D -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) -> z ~~ B ) )
40 21 39 jcad 
 |-  ( C = D -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) -> ( z ~~ A /\ z ~~ B ) ) )
41 ensym 
 |-  ( z ~~ A -> A ~~ z )
42 entr 
 |-  ( ( A ~~ z /\ z ~~ B ) -> A ~~ B )
43 41 42 sylan 
 |-  ( ( z ~~ A /\ z ~~ B ) -> A ~~ B )
44 40 43 syl6 
 |-  ( C = D -> ( ( z ~~ A /\ A. y ( y ~~ A -> ( rank ` z ) C_ ( rank ` y ) ) ) -> A ~~ B ) )
45 19 44 biimtrid 
 |-  ( C = D -> ( ( z e. { w | w ~~ A } /\ A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) ) -> A ~~ B ) )
46 45 expd 
 |-  ( C = D -> ( z e. { w | w ~~ A } -> ( A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) -> A ~~ B ) ) )
47 46 rexlimdv 
 |-  ( C = D -> ( E. z e. { w | w ~~ A } A. y e. { w | w ~~ A } ( rank ` z ) C_ ( rank ` y ) -> A ~~ B ) )
48 13 47 mpi 
 |-  ( C = D -> A ~~ B )
49 enen2 
 |-  ( A ~~ B -> ( x ~~ A <-> x ~~ B ) )
50 enen2 
 |-  ( A ~~ B -> ( y ~~ A <-> y ~~ B ) )
51 50 imbi1d 
 |-  ( A ~~ B -> ( ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) )
52 51 albidv 
 |-  ( A ~~ B -> ( A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) )
53 49 52 anbi12d 
 |-  ( A ~~ B -> ( ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) ) )
54 53 abbidv 
 |-  ( A ~~ B -> { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } )
55 54 2 3 3eqtr4g 
 |-  ( A ~~ B -> C = D )
56 48 55 impbii 
 |-  ( C = D <-> A ~~ B )