This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑆 )