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 ( 𝑇 , 𝑆 ) )