Metamath Proof Explorer

Theorem s3iunsndisj

Description: The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021)

Ref Expression
Assertion s3iunsndisj 
|- ( B e. X -> Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( a = d -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
2 1 a1d 
 |-  ( a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) ) )
3 eliun 
 |-  ( s e. U_ c e. ( Z \ { a } ) { <" a B c "> } <-> E. c e. ( Z \ { a } ) s e. { <" a B c "> } )
4 velsn 
 |-  ( s e. { <" a B c "> } <-> s = <" a B c "> )
5 eqeq1 
 |-  ( s = <" a B c "> -> ( s = <" d B e "> <-> <" a B c "> = <" d B e "> ) )
6 5 adantl 
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( s = <" d B e "> <-> <" a B c "> = <" d B e "> ) )
7 s3cli 
 |-  <" a B c "> e. Word _V
8 elex 
 |-  ( B e. X -> B e. _V )
9 elex 
 |-  ( d e. Y -> d e. _V )
10 9 adantl 
 |-  ( ( a e. Y /\ d e. Y ) -> d e. _V )
11 8 10 anim12ci 
 |-  ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( d e. _V /\ B e. _V ) )
12 elex 
 |-  ( e e. ( Z \ { d } ) -> e e. _V )
13 12 adantl 
 |-  ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> e e. _V )
14 11 13 anim12i 
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( ( d e. _V /\ B e. _V ) /\ e e. _V ) )
15 df-3an 
 |-  ( ( d e. _V /\ B e. _V /\ e e. _V ) <-> ( ( d e. _V /\ B e. _V ) /\ e e. _V ) )
16 14 15 sylibr 
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( d e. _V /\ B e. _V /\ e e. _V ) )
17 eqwrds3 
 |-  ( ( <" a B c "> e. Word _V /\ ( d e. _V /\ B e. _V /\ e e. _V ) ) -> ( <" a B c "> = <" d B e "> <-> ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) ) )
18 7 16 17 sylancr 
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( <" a B c "> = <" d B e "> <-> ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) ) )
19 s3fv0 
 |-  ( a e. _V -> ( <" a B c "> ` 0 ) = a )
20 19 elv 
 |-  ( <" a B c "> ` 0 ) = a
21 simp1 
 |-  ( ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) -> ( <" a B c "> ` 0 ) = d )
22 20 21 eqtr3id 
 |-  ( ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) -> a = d )
23 22 adantl 
 |-  ( ( ( # ` <" a B c "> ) = 3 /\ ( ( <" a B c "> ` 0 ) = d /\ ( <" a B c "> ` 1 ) = B /\ ( <" a B c "> ` 2 ) = e ) ) -> a = d )
24 18 23 syl6bi 
 |-  ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) -> ( <" a B c "> = <" d B e "> -> a = d ) )
25 24 adantr 
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( <" a B c "> = <" d B e "> -> a = d ) )
26 6 25 sylbid 
 |-  ( ( ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) /\ s = <" a B c "> ) -> ( s = <" d B e "> -> a = d ) )
27 26 ancoms 
 |-  ( ( s = <" a B c "> /\ ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) ) -> ( s = <" d B e "> -> a = d ) )
28 27 con3d 
 |-  ( ( s = <" a B c "> /\ ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) /\ ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) ) ) -> ( -. a = d -> -. s = <" d B e "> ) )
29 28 exp32 
 |-  ( s = <" a B c "> -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( -. a = d -> -. s = <" d B e "> ) ) ) )
30 29 com14 
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) ) )
31 30 imp 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( ( c e. ( Z \ { a } ) /\ e e. ( Z \ { d } ) ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) )
32 31 expd 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( c e. ( Z \ { a } ) -> ( e e. ( Z \ { d } ) -> ( s = <" a B c "> -> -. s = <" d B e "> ) ) ) )
33 32 com34 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( c e. ( Z \ { a } ) -> ( s = <" a B c "> -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) ) )
34 33 imp 
 |-  ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) -> ( s = <" a B c "> -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) )
35 4 34 syl5bi 
 |-  ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) -> ( s e. { <" a B c "> } -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) ) )
36 35 imp 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> ( e e. ( Z \ { d } ) -> -. s = <" d B e "> ) )
37 36 imp 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) /\ e e. ( Z \ { d } ) ) -> -. s = <" d B e "> )
38 velsn 
 |-  ( s e. { <" d B e "> } <-> s = <" d B e "> )
39 37 38 sylnibr 
 |-  ( ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) /\ e e. ( Z \ { d } ) ) -> -. s e. { <" d B e "> } )
40 39 nrexdv 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> -. E. e e. ( Z \ { d } ) s e. { <" d B e "> } )
41 eliun 
 |-  ( s e. U_ e e. ( Z \ { d } ) { <" d B e "> } <-> E. e e. ( Z \ { d } ) s e. { <" d B e "> } )
42 40 41 sylnibr 
 |-  ( ( ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) /\ c e. ( Z \ { a } ) ) /\ s e. { <" a B c "> } ) -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
43 42 rexlimdva2 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( E. c e. ( Z \ { a } ) s e. { <" a B c "> } -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } ) )
44 3 43 syl5bi 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } ) )
45 44 ralrimiv 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
46 eqidd 
 |-  ( c = e -> d = d )
47 eqidd 
 |-  ( c = e -> B = B )
48 id 
 |-  ( c = e -> c = e )
49 46 47 48 s3eqd 
 |-  ( c = e -> <" d B c "> = <" d B e "> )
50 49 sneqd 
 |-  ( c = e -> { <" d B c "> } = { <" d B e "> } )
51 50 cbviunv 
 |-  U_ c e. ( Z \ { d } ) { <" d B c "> } = U_ e e. ( Z \ { d } ) { <" d B e "> }
52 51 eleq2i 
 |-  ( s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
53 52 notbii 
 |-  ( -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
54 53 ralbii 
 |-  ( A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } <-> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ e e. ( Z \ { d } ) { <" d B e "> } )
55 45 54 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } )
56 disj 
 |-  ( ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) <-> A. s e. U_ c e. ( Z \ { a } ) { <" a B c "> } -. s e. U_ c e. ( Z \ { d } ) { <" d B c "> } )
57 55 56 sylibr 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) )
58 57 olcd 
 |-  ( ( -. a = d /\ ( B e. X /\ ( a e. Y /\ d e. Y ) ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
59 58 ex 
 |-  ( -. a = d -> ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) ) )
60 2 59 pm2.61i 
 |-  ( ( B e. X /\ ( a e. Y /\ d e. Y ) ) -> ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
61 60 ralrimivva 
 |-  ( B e. X -> A. a e. Y A. d e. Y ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
62 sneq 
 |-  ( a = d -> { a } = { d } )
63 62 difeq2d 
 |-  ( a = d -> ( Z \ { a } ) = ( Z \ { d } ) )
64 id 
 |-  ( a = d -> a = d )
65 eqidd 
 |-  ( a = d -> B = B )
66 eqidd 
 |-  ( a = d -> c = c )
67 64 65 66 s3eqd 
 |-  ( a = d -> <" a B c "> = <" d B c "> )
68 67 sneqd 
 |-  ( a = d -> { <" a B c "> } = { <" d B c "> } )
69 63 68 disjiunb 
 |-  ( Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } <-> A. a e. Y A. d e. Y ( a = d \/ ( U_ c e. ( Z \ { a } ) { <" a B c "> } i^i U_ c e. ( Z \ { d } ) { <" d B c "> } ) = (/) ) )
70 61 69 sylibr 
 |-  ( B e. X -> Disj_ a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } )