Theorem kardenOLD 9973

Description: Obsolete version of karden 9972 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.)

Hypotheses

Ref	Expression
kardenOLD.a	⊢ 𝐴 ∈ V
kardenOLD.c	⊢ 𝐶 = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
kardenOLD.d	⊢ 𝐷 = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}

Assertion

Ref	Expression
kardenOLD	⊢ (𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Allowed substitution hints:   𝐶(𝑥, 𝑦)   𝐷(𝑥, 𝑦)

Proof of Theorem kardenOLD

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kardenOLD.a	. . . . . . 7 ⊢ 𝐴 ∈ V
2		breq1 5109	. . . . . . 7 ⊢ (𝑤 = 𝐴 → (𝑤 ≈ 𝐴 ↔ 𝐴 ≈ 𝐴))
3	1	enref 9026	. . . . . . 7 ⊢ 𝐴 ≈ 𝐴
4	1, 2, 3	ceqsexv2d 3503	. . . . . 6 ⊢ ∃𝑤 𝑤 ≈ 𝐴
5		abn0 4337	. . . . . 6 ⊢ ({𝑤 ∣ 𝑤 ≈ 𝐴} ≠ ∅ ↔ ∃𝑤 𝑤 ≈ 𝐴)
6	4, 5	mpbir 234	. . . . 5 ⊢ {𝑤 ∣ 𝑤 ≈ 𝐴} ≠ ∅
7		scott0OLD 9951	. . . . . 6 ⊢ ({𝑤 ∣ 𝑤 ≈ 𝐴} = ∅ ↔ {𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∣ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} = ∅)
8	7	necon3bii 3011	. . . . 5 ⊢ ({𝑤 ∣ 𝑤 ≈ 𝐴} ≠ ∅ ↔ {𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∣ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅)
9	6, 8	mpbi 233	. . . 4 ⊢ {𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∣ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅
10		rabn0 4342	. . . 4 ⊢ ({𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∣ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)} ≠ ∅ ↔ ∃𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴}∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦))
11	9, 10	mpbi 233	. . 3 ⊢ ∃𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴}∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)
12		vex 3458	. . . . . . . 8 ⊢ 𝑧 ∈ V
13		breq1 5109	. . . . . . . 8 ⊢ (𝑤 = 𝑧 → (𝑤 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴))
14	12, 13	elab 3636	. . . . . . 7 ⊢ (𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ↔ 𝑧 ≈ 𝐴)
15		breq1 5109	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝑤 ≈ 𝐴 ↔ 𝑦 ≈ 𝐴))
16	15	ralab 3654	. . . . . . 7 ⊢ (∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) ↔ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))
17	14, 16	anbi12i 640	. . . . . 6 ⊢ ((𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∧ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) ↔ (𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
18		simpl 488	. . . . . . . . 9 ⊢ ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧 ≈ 𝐴)
19	18	a1i 11	. . . . . . . 8 ⊢ (𝐶 = 𝐷 → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧 ≈ 𝐴))
20		kardenOLD.c	. . . . . . . . . . . 12 ⊢ 𝐶 = {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
21		kardenOLD.d	. . . . . . . . . . . 12 ⊢ 𝐷 = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))}
22	20, 21	eqeq12i 2781	. . . . . . . . . . 11 ⊢ (𝐶 = 𝐷 ↔ {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
23		abbib 2832	. . . . . . . . . . 11 ⊢ ({𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑥((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
24	22, 23	bitri 278	. . . . . . . . . 10 ⊢ (𝐶 = 𝐷 ↔ ∀𝑥((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
25		breq1 5109	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ≈ 𝐴 ↔ 𝑧 ≈ 𝐴))
26		fveq2 6896	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑧 → (rank‘𝑥) = (rank‘𝑧))
27	26	sseq1d 3944	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑦)))
28	27	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ((𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
29	28	albidv 1954	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))))
30	25, 29	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
31		breq1 5109	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ≈ 𝐵 ↔ 𝑧 ≈ 𝐵))
32	27	imbi2d 343	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ((𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
33	32	albidv 1954	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))
34	31, 33	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → ((𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
35	30, 34	bibi12d 348	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) ↔ ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))))))
36	35	spvv 2022	. . . . . . . . . 10 ⊢ (∀𝑥((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))) → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
37	24, 36	sylbi 220	. . . . . . . . 9 ⊢ (𝐶 = 𝐷 → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) ↔ (𝑧 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦)))))
38		simpl 488	. . . . . . . . 9 ⊢ ((𝑧 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧 ≈ 𝐵)
39	37, 38	biimtrdi 256	. . . . . . . 8 ⊢ (𝐶 = 𝐷 → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝑧 ≈ 𝐵))
40	19, 39	jcad 522	. . . . . . 7 ⊢ (𝐶 = 𝐷 → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → (𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵)))
41		ensym 9044	. . . . . . . 8 ⊢ (𝑧 ≈ 𝐴 → 𝐴 ≈ 𝑧)
42		entr 9047	. . . . . . . 8 ⊢ ((𝐴 ≈ 𝑧 ∧ 𝑧 ≈ 𝐵) → 𝐴 ≈ 𝐵)
43	41, 42	sylan 592	. . . . . . 7 ⊢ ((𝑧 ≈ 𝐴 ∧ 𝑧 ≈ 𝐵) → 𝐴 ≈ 𝐵)
44	40, 43	syl6 36	. . . . . 6 ⊢ (𝐶 = 𝐷 → ((𝑧 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑧) ⊆ (rank‘𝑦))) → 𝐴 ≈ 𝐵))
45	17, 44	biimtrid 245	. . . . 5 ⊢ (𝐶 = 𝐷 → ((𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} ∧ ∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦)) → 𝐴 ≈ 𝐵))
46	45	expd 421	. . . 4 ⊢ (𝐶 = 𝐷 → (𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} → (∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴 ≈ 𝐵)))
47	46	rexlimdv 3165	. . 3 ⊢ (𝐶 = 𝐷 → (∃𝑧 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴}∀𝑦 ∈ {𝑤 ∣ 𝑤 ≈ 𝐴} (rank‘𝑧) ⊆ (rank‘𝑦) → 𝐴 ≈ 𝐵))
48	11, 47	mpi 21	. 2 ⊢ (𝐶 = 𝐷 → 𝐴 ≈ 𝐵)
49		enen2 9151	. . . . 5 ⊢ (𝐴 ≈ 𝐵 → (𝑥 ≈ 𝐴 ↔ 𝑥 ≈ 𝐵))
50		enen2 9151	. . . . . . 7 ⊢ (𝐴 ≈ 𝐵 → (𝑦 ≈ 𝐴 ↔ 𝑦 ≈ 𝐵))
51	50	imbi1d 344	. . . . . 6 ⊢ (𝐴 ≈ 𝐵 → ((𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
52	51	albidv 1954	. . . . 5 ⊢ (𝐴 ≈ 𝐵 → (∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦))))
53	49, 52	anbi12d 644	. . . 4 ⊢ (𝐴 ≈ 𝐵 → ((𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))))
54	53	abbidv 2829	. . 3 ⊢ (𝐴 ≈ 𝐵 → {𝑥 ∣ (𝑥 ≈ 𝐴 ∧ ∀𝑦(𝑦 ≈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦)))} = {𝑥 ∣ (𝑥 ≈ 𝐵 ∧ ∀𝑦(𝑦 ≈ 𝐵 → (rank‘𝑥) ⊆ (rank‘𝑦)))})
55	54, 20, 21	3eqtr4g 2823	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐶 = 𝐷)
56	48, 55	impbii 212	1 ⊢ (𝐶 = 𝐷 ↔ 𝐴 ≈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2146  {cab 2741   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900  ∅c0 4281   class class class wbr 5106  ‘cfv 6547   ≈ cen 8984  rankcrnk 9780

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-ov 7433  df-om 7888  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-er 8731  df-en 8988  df-r1 9781  df-rank 9782

This theorem is used by: (None)