Metamath Proof Explorer

Theorem cantnffval2

Description: An alternate definition of df-cnf which relies on cantnf . (Note that although the use of S seems self-referential, one can use cantnfdm to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
Assertion cantnffval2 ⊢ φ → A CNF B = OrdIso T S -1

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 1 2 3 4 cantnf ⊢ φ → A CNF B Isom T , E S A ↑ 𝑜 B
6 isof1o ⊢ A CNF B Isom T , E S A ↑ 𝑜 B → A CNF B : S ⟶ 1-1 onto A ↑ 𝑜 B
7 f1orel ⊢ A CNF B : S ⟶ 1-1 onto A ↑ 𝑜 B → Rel ⁡ A CNF B
8 5 6 7 3syl ⊢ φ → Rel ⁡ A CNF B
9 dfrel2 ⊢ Rel ⁡ A CNF B ↔ A CNF B -1 -1 = A CNF B
10 8 9 sylib ⊢ φ → A CNF B -1 -1 = A CNF B
11 oecl ⊢ A ∈ On ∧ B ∈ On → A ↑ 𝑜 B ∈ On
12 2 3 11 syl2anc ⊢ φ → A ↑ 𝑜 B ∈ On
13 eloni ⊢ A ↑ 𝑜 B ∈ On → Ord ⁡ A ↑ 𝑜 B
14 12 13 syl ⊢ φ → Ord ⁡ A ↑ 𝑜 B
15 isocnv ⊢ A CNF B Isom T , E S A ↑ 𝑜 B → A CNF B -1 Isom E , T A ↑ 𝑜 B S
16 5 15 syl ⊢ φ → A CNF B -1 Isom E , T A ↑ 𝑜 B S
17 1 2 3 4 oemapwe ⊢ φ → T We S ∧ dom ⁡ OrdIso T S = A ↑ 𝑜 B
18 17 simpld ⊢ φ → T We S
19 ovex ⊢ A CNF B ∈ V
20 19 dmex ⊢ dom ⁡ A CNF B ∈ V
21 1 20 eqeltri ⊢ S ∈ V
22 exse ⊢ S ∈ V → T Se S
23 21 22 ax-mp ⊢ T Se S
24 eqid ⊢ OrdIso T S = OrdIso T S
25 24 oieu ⊢ T We S ∧ T Se S → Ord ⁡ A ↑ 𝑜 B ∧ A CNF B -1 Isom E , T A ↑ 𝑜 B S ↔ A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
26 18 23 25 sylancl ⊢ φ → Ord ⁡ A ↑ 𝑜 B ∧ A CNF B -1 Isom E , T A ↑ 𝑜 B S ↔ A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
27 14 16 26 mpbi2and ⊢ φ → A ↑ 𝑜 B = dom ⁡ OrdIso T S ∧ A CNF B -1 = OrdIso T S
28 27 simprd ⊢ φ → A CNF B -1 = OrdIso T S
29 28 cnveqd ⊢ φ → A CNF B -1 -1 = OrdIso T S -1
30 10 29 eqtr3d ⊢ φ → A CNF B = OrdIso T S -1