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	syl5eq	⊢ ( 𝜑 → 𝑆 = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
35		soeq2	⊢ ( 𝑆 = { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } → ( 𝑇 Or 𝑆 ↔ 𝑇 Or { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
36	34 35	syl	⊢ ( 𝜑 → ( 𝑇 Or 𝑆 ↔ 𝑇 Or { 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
37	31 36	mpbird	⊢ ( 𝜑 → 𝑇 Or 𝑆 )