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 ⊢ 𝐴 ∈ V
kardenOLD.c ⊢ 𝐶 = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
kardenOLD.d ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
Assertion kardenOLD ( 𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵 )

Proof

Step Hyp Ref Expression
1 kardenOLD.a ⊢ 𝐴 ∈ V
2 kardenOLD.c ⊢ 𝐶 = { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
3 kardenOLD.d ⊢ 𝐷 = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
4 breq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴 ) )
5 1 enref ⊢ 𝐴 ≈ 𝐴
6 1 4 5 ceqsexv2d ⊢ ∃ 𝑤 𝑤 ≈ 𝐴
7 abn0 ⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅ ↔ ∃ 𝑤 𝑤 ≈ 𝐴 )
8 6 7 mpbir ⊢ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅
9 scott0OLD ⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } = ∅ ↔ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
10 9 necon3bii ⊢ ( { 𝑤 ∣ 𝑤 ≈ 𝐴 } ≠ ∅ ↔ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )
11 8 10 mpbi ⊢ { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅
12 rabn0 ⊢ ( { 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∣ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) )
13 11 12 mpbi ⊢ ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
14 vex ⊢ 𝑧 ∈ V
15 breq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴 ) )
16 14 15 elab ⊢ ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ↔ 𝑧 ≈ 𝐴 )
17 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ≈ 𝐴 ↔ 𝑦 ≈ 𝐴 ) )
18 17 ralab ⊢ ( ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) )
19 16 18 anbi12i ⊢ ( ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
20 simpl ⊢ ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐴 )
21 20 a1i ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐴 ) )
22 2 3 eqeq12i ⊢ ( 𝐶 = 𝐷 ↔ { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
23 abbib ⊢ ( { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ↔ ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
24 22 23 bitri ⊢ ( 𝐶 = 𝐷 ↔ ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
25 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴 ) )
26 fveq2 ⊢ ( 𝑥 = 𝑧 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑧 ) )
27 26 sseq1d ⊢ ( 𝑥 = 𝑧 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) )
28 27 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
29 28 albidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
30 25 29 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
31 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≈ 𝐵 ↔ 𝑧 ≈ 𝐵 ) )
32 27 imbi2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
33 32 albidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
34 31 33 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
35 30 34 bibi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) ) )
36 35 spvv ⊢ ( ∀ 𝑥 ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
37 24 36 sylbi ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
38 simpl ⊢ ( ( 𝑧 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐵 )
39 37 38 biimtrdi ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝑧 ≈ 𝐵 ) )
40 21 39 jcad ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → ( 𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵 ) ) )
41 ensym ⊢ ( 𝑧 ≈ 𝐴 → 𝐴 ≈ 𝑧 )
42 entr ⊢ ( ( 𝐴 ≈ 𝑧 ∧ 𝑧 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
43 41 42 sylan ⊢ ( ( 𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵 ) → 𝐴 ≈ 𝐵 )
44 40 43 syl6 ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) ) → 𝐴 ≈ 𝐵 ) )
45 19 44 biimtrid ⊢ ( 𝐶 = 𝐷 → ( ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ) → 𝐴 ≈ 𝐵 ) )
46 45 expd ⊢ ( 𝐶 = 𝐷 → ( 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } → ( ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) → 𝐴 ≈ 𝐵 ) ) )
47 46 rexlimdv ⊢ ( 𝐶 = 𝐷 → ( ∃ 𝑧 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ∀ 𝑦 ∈ { 𝑤 ∣ 𝑤 ≈ 𝐴 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) → 𝐴 ≈ 𝐵 ) )
48 13 47 mpi ⊢ ( 𝐶 = 𝐷 → 𝐴 ≈ 𝐵 )
49 enen2 ⊢ ( 𝐴 ≈ 𝐵 → ( 𝑥 ≈ 𝐴 ↔ 𝑥 ≈ 𝐵 ) )
50 enen2 ⊢ ( 𝐴 ≈ 𝐵 → ( 𝑦 ≈ 𝐴 ↔ 𝑦 ≈ 𝐵 ) )
51 50 imbi1d ⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
52 51 albidv ⊢ ( 𝐴 ≈ 𝐵 → ( ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
53 49 52 anbi12d ⊢ ( 𝐴 ≈ 𝐵 → ( ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ↔ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) ) )
54 53 abbidv ⊢ ( 𝐴 ≈ 𝐵 → { 𝑥 ∣ ( 𝑥 ≈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = { 𝑥 ∣ ( 𝑥 ≈ 𝐵 ∧ ∀ 𝑦 ( 𝑦 ≈ 𝐵 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } )
55 54 2 3 3eqtr4g ⊢ ( 𝐴 ≈ 𝐵 → 𝐶 = 𝐷 )
56 48 55 impbii ⊢ ( 𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵 )