Theorem sofld

Description: The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	sofld	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 = ( dom 𝑅 ∪ ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relxp	⊢ Rel ( 𝐴 × 𝐴 )
2		relss	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ( Rel ( 𝐴 × 𝐴 ) → Rel 𝑅 ) )
3	1 2	mpi	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → Rel 𝑅 )
4	3	ad2antlr	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → Rel 𝑅 )
5		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
6		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑥 } )
7		undif1	⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } )
8	6 7	sseqtrri	⊢ 𝐴 ⊆ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } )
9		simpll	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑅 Or 𝐴 )
10		dmss	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → dom 𝑅 ⊆ dom ( 𝐴 × 𝐴 ) )
11		dmxpid	⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
12	10 11	sseqtrdi	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → dom 𝑅 ⊆ 𝐴 )
13	12	ad2antlr	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → dom 𝑅 ⊆ 𝐴 )
14	3	ad2antlr	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → Rel 𝑅 )
15		releldm	⊢ ( ( Rel 𝑅 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
16	14 15	sylancom	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
17	13 16	sseldd	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐴 )
18		sossfld	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
19	9 17 18	syl2anc	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
20		ssun1	⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
21	20 16	sselid	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
22	21	snssd	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → { 𝑥 } ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
23	19 22	unssd	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
24	8 23	sstrid	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
25	24	ex	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
26	5 25	syl5bir	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
27	26	con3dimp	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
28	27	pm2.21d	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
29	4 28	relssdv	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝑅 ⊆ ∅ )
30		ss0	⊢ ( 𝑅 ⊆ ∅ → 𝑅 = ∅ )
31	29 30	syl	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝑅 = ∅ )
32	31	ex	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) → 𝑅 = ∅ ) )
33	32	necon1ad	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( 𝑅 ≠ ∅ → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34	33	3impia	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
35		rnss	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ran 𝑅 ⊆ ran ( 𝐴 × 𝐴 ) )
36		rnxpid	⊢ ran ( 𝐴 × 𝐴 ) = 𝐴
37	35 36	sseqtrdi	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ran 𝑅 ⊆ 𝐴 )
38	12 37	unssd	⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ( dom 𝑅 ∪ ran 𝑅 ) ⊆ 𝐴 )
39	38	3ad2ant2	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → ( dom 𝑅 ∪ ran 𝑅 ) ⊆ 𝐴 )
40	34 39	eqssd	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 = ( dom 𝑅 ∪ ran 𝑅 ) )