Metamath Proof Explorer

Theorem fiunlem

Description: Lemma for fiun and f1iun . Formerly part of f1iun . (Contributed by AV, 6-Oct-2023)

Ref Expression
Hypothesis fiun.1 
|- ( x = y -> B = C )
Assertion fiunlem 
|- ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) )

Proof

Step Hyp Ref Expression
1 fiun.1 
 |-  ( x = y -> B = C )
2 vex 
 |-  v e. _V
3 eqeq1 
 |-  ( z = v -> ( z = B <-> v = B ) )
4 3 rexbidv 
 |-  ( z = v -> ( E. x e. A z = B <-> E. x e. A v = B ) )
5 2 4 elab 
 |-  ( v e. { z | E. x e. A z = B } <-> E. x e. A v = B )
6 1 eqeq2d 
 |-  ( x = y -> ( v = B <-> v = C ) )
7 6 cbvrexvw 
 |-  ( E. x e. A v = B <-> E. y e. A v = C )
8 r19.29 
 |-  ( ( A. y e. A ( B C_ C \/ C C_ B ) /\ E. y e. A v = C ) -> E. y e. A ( ( B C_ C \/ C C_ B ) /\ v = C ) )
9 sseq12 
 |-  ( ( u = B /\ v = C ) -> ( u C_ v <-> B C_ C ) )
10 9 ancoms 
 |-  ( ( v = C /\ u = B ) -> ( u C_ v <-> B C_ C ) )
11 sseq12 
 |-  ( ( v = C /\ u = B ) -> ( v C_ u <-> C C_ B ) )
12 10 11 orbi12d 
 |-  ( ( v = C /\ u = B ) -> ( ( u C_ v \/ v C_ u ) <-> ( B C_ C \/ C C_ B ) ) )
13 12 biimprcd 
 |-  ( ( B C_ C \/ C C_ B ) -> ( ( v = C /\ u = B ) -> ( u C_ v \/ v C_ u ) ) )
14 13 expdimp 
 |-  ( ( ( B C_ C \/ C C_ B ) /\ v = C ) -> ( u = B -> ( u C_ v \/ v C_ u ) ) )
15 14 rexlimivw 
 |-  ( E. y e. A ( ( B C_ C \/ C C_ B ) /\ v = C ) -> ( u = B -> ( u C_ v \/ v C_ u ) ) )
16 15 imp 
 |-  ( ( E. y e. A ( ( B C_ C \/ C C_ B ) /\ v = C ) /\ u = B ) -> ( u C_ v \/ v C_ u ) )
17 8 16 sylan 
 |-  ( ( ( A. y e. A ( B C_ C \/ C C_ B ) /\ E. y e. A v = C ) /\ u = B ) -> ( u C_ v \/ v C_ u ) )
18 17 an32s 
 |-  ( ( ( A. y e. A ( B C_ C \/ C C_ B ) /\ u = B ) /\ E. y e. A v = C ) -> ( u C_ v \/ v C_ u ) )
19 18 adantlll 
 |-  ( ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) /\ E. y e. A v = C ) -> ( u C_ v \/ v C_ u ) )
20 7 19 sylan2b 
 |-  ( ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) /\ E. x e. A v = B ) -> ( u C_ v \/ v C_ u ) )
21 5 20 sylan2b 
 |-  ( ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) /\ v e. { z | E. x e. A z = B } ) -> ( u C_ v \/ v C_ u ) )
22 21 ralrimiva 
 |-  ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) ) /\ u = B ) -> A. v e. { z | E. x e. A z = B } ( u C_ v \/ v C_ u ) )