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) (Revised by AV, 21-Jul-2024)

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

Proof

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

Metamath Proof Explorer

Theorem wemapso

Proof