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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
Assertion cantnffval2 ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ◡ OrdIso ( 𝑇 , 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 oemapval.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5 1 2 3 4 cantnf ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) )
6 isof1o ⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) )
7 f1orel ⊢ ( ( 𝐴 CNF 𝐵 ) : 𝑆 –1-1-onto→ ( 𝐴 ↑o 𝐵 ) → Rel ( 𝐴 CNF 𝐵 ) )
8 5 6 7 3syl ⊢ ( 𝜑 → Rel ( 𝐴 CNF 𝐵 ) )
9 dfrel2 ⊢ ( Rel ( 𝐴 CNF 𝐵 ) ↔ ◡ ◡ ( 𝐴 CNF 𝐵 ) = ( 𝐴 CNF 𝐵 ) )
10 8 9 sylib ⊢ ( 𝜑 → ◡ ◡ ( 𝐴 CNF 𝐵 ) = ( 𝐴 CNF 𝐵 ) )
11 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
12 2 3 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 ↑o 𝐵 ) ∈ On )
13 eloni ⊢ ( ( 𝐴 ↑o 𝐵 ) ∈ On → Ord ( 𝐴 ↑o 𝐵 ) )
14 12 13 syl ⊢ ( 𝜑 → Ord ( 𝐴 ↑o 𝐵 ) )
15 isocnv ⊢ ( ( 𝐴 CNF 𝐵 ) Isom 𝑇 , E ( 𝑆 , ( 𝐴 ↑o 𝐵 ) ) → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) )
16 5 15 syl ⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) )
17 1 2 3 4 oemapwe ⊢ ( 𝜑 → ( 𝑇 We 𝑆 ∧ dom OrdIso ( 𝑇 , 𝑆 ) = ( 𝐴 ↑o 𝐵 ) ) )
18 17 simpld ⊢ ( 𝜑 → 𝑇 We 𝑆 )
19 ovex ⊢ ( 𝐴 CNF 𝐵 ) ∈ V
20 19 dmex ⊢ dom ( 𝐴 CNF 𝐵 ) ∈ V
21 1 20 eqeltri ⊢ 𝑆 ∈ V
22 exse ⊢ ( 𝑆 ∈ V → 𝑇 Se 𝑆 )
23 21 22 ax-mp ⊢ 𝑇 Se 𝑆
24 eqid ⊢ OrdIso ( 𝑇 , 𝑆 ) = OrdIso ( 𝑇 , 𝑆 )
25 24 oieu ⊢ ( ( 𝑇 We 𝑆 ∧ 𝑇 Se 𝑆 ) → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) )
26 18 23 25 sylancl ⊢ ( 𝜑 → ( ( Ord ( 𝐴 ↑o 𝐵 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) Isom E , 𝑇 ( ( 𝐴 ↑o 𝐵 ) , 𝑆 ) ) ↔ ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) ) )
27 14 16 26 mpbi2and ⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝐵 ) = dom OrdIso ( 𝑇 , 𝑆 ) ∧ ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) ) )
28 27 simprd ⊢ ( 𝜑 → ◡ ( 𝐴 CNF 𝐵 ) = OrdIso ( 𝑇 , 𝑆 ) )
29 28 cnveqd ⊢ ( 𝜑 → ◡ ◡ ( 𝐴 CNF 𝐵 ) = ◡ OrdIso ( 𝑇 , 𝑆 ) )
30 10 29 eqtr3d ⊢ ( 𝜑 → ( 𝐴 CNF 𝐵 ) = ◡ OrdIso ( 𝑇 , 𝑆 ) )