Metamath Proof Explorer


Theorem oemapso

Description: The relation T is a strict order on S (a corollary of wemapso2 ). (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ( 𝜑𝐴 ∈ On )
cantnfs.b ( 𝜑𝐵 ∈ On )
oemapval.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
Assertion oemapso ( 𝜑𝑇 Or 𝑆 )

Proof

Step Hyp Ref Expression
1 cantnfs.s 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ( 𝜑𝐴 ∈ On )
3 cantnfs.b ( 𝜑𝐵 ∈ On )
4 oemapval.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
5 eloni ( 𝐵 ∈ On → Ord 𝐵 )
6 ordwe ( Ord 𝐵 → E We 𝐵 )
7 weso ( E We 𝐵 → E Or 𝐵 )
8 3 5 6 7 4syl ( 𝜑 → E Or 𝐵 )
9 cnvso ( E Or 𝐵 E Or 𝐵 )
10 8 9 sylib ( 𝜑 E Or 𝐵 )
11 eloni ( 𝐴 ∈ On → Ord 𝐴 )
12 ordwe ( Ord 𝐴 → E We 𝐴 )
13 weso ( E We 𝐴 → E Or 𝐴 )
14 2 11 12 13 4syl ( 𝜑 → E Or 𝐴 )
15 fvex ( 𝑦𝑧 ) ∈ V
16 15 epeli ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ↔ ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) )
17 vex 𝑤 ∈ V
18 vex 𝑧 ∈ V
19 17 18 brcnv ( 𝑤 E 𝑧𝑧 E 𝑤 )
20 epel ( 𝑧 E 𝑤𝑧𝑤 )
21 19 20 bitri ( 𝑤 E 𝑧𝑧𝑤 )
22 21 imbi1i ( ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) )
23 22 ralbii ( ∀ 𝑤𝐵 ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ↔ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) )
24 16 23 anbi12i ( ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
25 24 rexbii ( ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
26 25 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) ∈ ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑧𝑤 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
27 4 26 eqtr4i 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧𝐵 ( ( 𝑥𝑧 ) E ( 𝑦𝑧 ) ∧ ∀ 𝑤𝐵 ( 𝑤 E 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) }
28 breq1 ( 𝑔 = 𝑥 → ( 𝑔 finSupp ∅ ↔ 𝑥 finSupp ∅ ) )
29 28 cbvrabv { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑥 ∈ ( 𝐴m 𝐵 ) ∣ 𝑥 finSupp ∅ }
30 27 29 wemapso2 ( ( 𝐵 ∈ On ∧ E Or 𝐵 ∧ E Or 𝐴 ) → 𝑇 Or { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
31 3 10 14 30 syl3anc ( 𝜑𝑇 Or { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
32 eqid { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ }
33 32 2 3 cantnfdm ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
34 1 33 eqtrid ( 𝜑𝑆 = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
35 soeq2 ( 𝑆 = { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } → ( 𝑇 Or 𝑆𝑇 Or { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
36 34 35 syl ( 𝜑 → ( 𝑇 Or 𝑆𝑇 Or { 𝑔 ∈ ( 𝐴m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
37 31 36 mpbird ( 𝜑𝑇 Or 𝑆 )