Theorem eupth2lem2

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015)

	Ref	Expression
Hypothesis	eupth2lem2.1	⊢ 𝐵 ∈ V
Assertion	eupth2lem2	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		eupth2lem2.1	⊢ 𝐵 ∈ V
2		eqidd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 = 𝐵 )
3	2	olcd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) )
4	3	biantrud	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
5		eupth2lem1	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
6	1 5	ax-mp	⊢ ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) )
7	4 6	bitr4di	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
8		simpr	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 = 𝑈 )
9	8	eleq1d	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
10	7 9	bitrd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
11	10	necon1bbid	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝐴 = 𝐵 ) )
12		simpl	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 ≠ 𝐶 )
13		neeq1	⊢ ( 𝐵 = 𝐴 → ( 𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
14	12 13	syl5ibcom	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 → 𝐴 ≠ 𝐶 ) )
15	14	pm4.71rd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 = 𝐴 ) ) )
16		eqcom	⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
17		ancom	⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 = 𝐴 ) )
18	15 16 17	3bitr4g	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ) )
19	12	neneqd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ¬ 𝐵 = 𝐶 )
20		biorf	⊢ ( ¬ 𝐵 = 𝐶 → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ) )
21	19 20	syl	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ) )
22		orcom	⊢ ( ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) )
23	21 22	bitrdi	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
24	23	anbi1d	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) ) )
25	18 24	bitrd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) ) )
26		ancom	⊢ ( ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) )
27	25 26	bitr4di	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ) )
28		eupth2lem1	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ) )
29	1 28	ax-mp	⊢ ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
30	8	eleq1d	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )
31	29 30	bitr3id	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )
32	11 27 31	3bitrd	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )