Theorem fin23lem24

Description: Lemma for fin23 . In a class of ordinals, each element is fully identified by those of its predecessors which also belong to the class. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Assertion	fin23lem24	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) = ( 𝐷 ∩ 𝐵 ) ↔ 𝐶 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → Ord 𝐴 )
2		simplr	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐵 ⊆ 𝐴 )
3		simprl	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐵 )
4	2 3	sseldd	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐴 )
5		ordelord	⊢ ( ( Ord 𝐴 ∧ 𝐶 ∈ 𝐴 ) → Ord 𝐶 )
6	1 4 5	syl2anc	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → Ord 𝐶 )
7		simprr	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐷 ∈ 𝐵 )
8	2 7	sseldd	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → 𝐷 ∈ 𝐴 )
9		ordelord	⊢ ( ( Ord 𝐴 ∧ 𝐷 ∈ 𝐴 ) → Ord 𝐷 )
10	1 8 9	syl2anc	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → Ord 𝐷 )
11		ordtri3	⊢ ( ( Ord 𝐶 ∧ Ord 𝐷 ) → ( 𝐶 = 𝐷 ↔ ¬ ( 𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶 ) ) )
12	11	necon2abid	⊢ ( ( Ord 𝐶 ∧ Ord 𝐷 ) → ( ( 𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶 ) ↔ 𝐶 ≠ 𝐷 ) )
13	6 10 12	syl2anc	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶 ) ↔ 𝐶 ≠ 𝐷 ) )
14		simpr	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ 𝐷 )
15		simplrl	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ 𝐵 )
16	14 15	elind	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → 𝐶 ∈ ( 𝐷 ∩ 𝐵 ) )
17	6	adantr	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → Ord 𝐶 )
18		ordirr	⊢ ( Ord 𝐶 → ¬ 𝐶 ∈ 𝐶 )
19	17 18	syl	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → ¬ 𝐶 ∈ 𝐶 )
20		elinel1	⊢ ( 𝐶 ∈ ( 𝐶 ∩ 𝐵 ) → 𝐶 ∈ 𝐶 )
21	19 20	nsyl	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → ¬ 𝐶 ∈ ( 𝐶 ∩ 𝐵 ) )
22		nelne1	⊢ ( ( 𝐶 ∈ ( 𝐷 ∩ 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐶 ∩ 𝐵 ) ) → ( 𝐷 ∩ 𝐵 ) ≠ ( 𝐶 ∩ 𝐵 ) )
23	16 21 22	syl2anc	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → ( 𝐷 ∩ 𝐵 ) ≠ ( 𝐶 ∩ 𝐵 ) )
24	23	necomd	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐶 ∈ 𝐷 ) → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) )
25		simpr	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → 𝐷 ∈ 𝐶 )
26		simplrr	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → 𝐷 ∈ 𝐵 )
27	25 26	elind	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → 𝐷 ∈ ( 𝐶 ∩ 𝐵 ) )
28	10	adantr	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → Ord 𝐷 )
29		ordirr	⊢ ( Ord 𝐷 → ¬ 𝐷 ∈ 𝐷 )
30	28 29	syl	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → ¬ 𝐷 ∈ 𝐷 )
31		elinel1	⊢ ( 𝐷 ∈ ( 𝐷 ∩ 𝐵 ) → 𝐷 ∈ 𝐷 )
32	30 31	nsyl	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → ¬ 𝐷 ∈ ( 𝐷 ∩ 𝐵 ) )
33		nelne1	⊢ ( ( 𝐷 ∈ ( 𝐶 ∩ 𝐵 ) ∧ ¬ 𝐷 ∈ ( 𝐷 ∩ 𝐵 ) ) → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) )
34	27 32 33	syl2anc	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ 𝐷 ∈ 𝐶 ) → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) )
35	24 34	jaodan	⊢ ( ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) ∧ ( 𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶 ) ) → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) )
36	35	ex	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∈ 𝐷 ∨ 𝐷 ∈ 𝐶 ) → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) ) )
37	13 36	sylbird	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( 𝐶 ≠ 𝐷 → ( 𝐶 ∩ 𝐵 ) ≠ ( 𝐷 ∩ 𝐵 ) ) )
38	37	necon4d	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) = ( 𝐷 ∩ 𝐵 ) → 𝐶 = 𝐷 ) )
39		ineq1	⊢ ( 𝐶 = 𝐷 → ( 𝐶 ∩ 𝐵 ) = ( 𝐷 ∩ 𝐵 ) )
40	38 39	impbid1	⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) = ( 𝐷 ∩ 𝐵 ) ↔ 𝐶 = 𝐷 ) )