Theorem wemapso

Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-2015)

	Ref	Expression
Hypothesis	wemapso.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
Assertion	wemapso	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		wemapso.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
2		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3		ssid	⊢ ( 𝐵 ↑m 𝐴 ) ⊆ ( 𝐵 ↑m 𝐴 )
4		simp1	⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝐴 ∈ V )
5		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑅 Or 𝐴 )
7		simp3	⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑆 Or 𝐵 )
8		simpl1	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝐴 ∈ V )
9		difss	⊢ ( 𝑎 ∖ 𝑏 ) ⊆ 𝑎
10		dmss	⊢ ( ( 𝑎 ∖ 𝑏 ) ⊆ 𝑎 → dom ( 𝑎 ∖ 𝑏 ) ⊆ dom 𝑎 )
11	9 10	ax-mp	⊢ dom ( 𝑎 ∖ 𝑏 ) ⊆ dom 𝑎
12		simprll	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) )
13		elmapi	⊢ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑎 : 𝐴 ⟶ 𝐵 )
14	12 13	syl	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 : 𝐴 ⟶ 𝐵 )
15	11 14	fssdm	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → dom ( 𝑎 ∖ 𝑏 ) ⊆ 𝐴 )
16	8 15	ssexd	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → dom ( 𝑎 ∖ 𝑏 ) ∈ V )
17		simpl2	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑅 We 𝐴 )
18		wefr	⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
19	17 18	syl	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑅 Fr 𝐴 )
20		simprr	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ≠ 𝑏 )
21	14	ffnd	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 Fn 𝐴 )
22		simprlr	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) )
23		elmapi	⊢ ( 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑏 : 𝐴 ⟶ 𝐵 )
24	22 23	syl	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 : 𝐴 ⟶ 𝐵 )
25	24	ffnd	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 Fn 𝐴 )
26		fndmdifeq0	⊢ ( ( 𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴 ) → ( dom ( 𝑎 ∖ 𝑏 ) = ∅ ↔ 𝑎 = 𝑏 ) )
27	21 25 26	syl2anc	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → ( dom ( 𝑎 ∖ 𝑏 ) = ∅ ↔ 𝑎 = 𝑏 ) )
28	27	necon3bid	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → ( dom ( 𝑎 ∖ 𝑏 ) ≠ ∅ ↔ 𝑎 ≠ 𝑏 ) )
29	20 28	mpbird	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → dom ( 𝑎 ∖ 𝑏 ) ≠ ∅ )
30		fri	⊢ ( ( ( dom ( 𝑎 ∖ 𝑏 ) ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( dom ( 𝑎 ∖ 𝑏 ) ⊆ 𝐴 ∧ dom ( 𝑎 ∖ 𝑏 ) ≠ ∅ ) ) → ∃ 𝑐 ∈ dom ( 𝑎 ∖ 𝑏 ) ∀ 𝑑 ∈ dom ( 𝑎 ∖ 𝑏 ) ¬ 𝑑 𝑅 𝑐 )
31	16 19 15 29 30	syl22anc	⊢ ( ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑎 ≠ 𝑏 ) ) → ∃ 𝑐 ∈ dom ( 𝑎 ∖ 𝑏 ) ∀ 𝑑 ∈ dom ( 𝑎 ∖ 𝑏 ) ¬ 𝑑 𝑅 𝑐 )
32	1 3 4 6 7 31	wemapsolem	⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐵 ↑m 𝐴 ) )
33	2 32	syl3an1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 We 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐵 ↑m 𝐴 ) )